Process journal of learning by Attila Vajda

ajourdhui

something cool #

I noticed, playing the Natural Number Game, and thinking about solving 0 + σd = σd using only add_zero, succ_eq_add_one, and add_succ is there seemed to be a sort of invisible pattern in which you could move the components

another cool thing #

The basic possible moves seem to be sort of factors. The basic possible moves seem to be sort of factors. I don't yet know which it is, add_zero, rw, induction, rfl, add_succ succ_eq_add_one, perhaps the minimum moves that are required to have the ℕ I guess

0 : ℕ
σ: ℕ ⟶ ℕ
induction

I still find it weird #

that we assume 0 + d = d so we can replace 0 + d in σ(0 + d) = d

show ∀n, 0 + n = n by induction 0 + 0 = 0 0 = 0 // add_zero assuming 0 + n = n // why

Oh maybe it's because if 0+n =n is true, 0+(n+ 1)=n + 1 cannot be false. if P, Q in ℕ ∀n∃σn, so if n∈ℕ, (n+1)∈ℕ and if the consequent of an implication is false, while the antecedent is true, then the implication is false

The implication has to be true, because that's a condition for being a member of ℕ

Okay I think I figured it out:

(P0 ∧ ∀n(Pn ⟶ Pσn)) ⟶ ∀nPn

P0 is true, because 0 + 0 = 0, by add_zero Pn ⟶ Pσn is false only if Pn ∧ ¬Pσn, because when ¬Pn the implication is true, and Pn ∧ Pσn the implication is true also, so we test for this possibility Pn ∧ ¬Pσn and see what happens when Pn is true, in this example it means we assume 0 + n = n is true, so we can replace occurrences of 0 + n with n and the consequent 0 + σn = σn will be either true or false, and if it is false, the implication is false, otherwise it is true.