On Jul 31, 9:49 am, Bruno Marchal <marc...@ulb.ac.be> wrote: > In which theory? > > The notion of proof is theory and definition dependent. (contrary to > computability, which is absolute, by Church thesis). > > If you agree to define x < y by Ez(z+x = y) "E" = "It exists". I > assume classical logic + the axioms: > > x+0 = x > x+s(y) = s(x+y) > > 0 denotes the number zero, and s(x) denotes the successor of x, often > noted as x+1. Cf the whole theory I gave last week. I use only a > subset of that theory here. > > So we have to prove that 0 < s(0). By the definition of "<" above, we > have to prove that Ez(z + 0 = s(0)) > But s(0) + 0 = s(0) by the axiom x + 0 = x given above. > So Ez(0 + z = s(0)) is true, with z = s(0). (This is the usual use of > the existence rule of classical logic). > > Of course we could have taken the theory with the unique axiom "1 is > greater than 0". For all proposition we can always find a theory which > proves it. The interesting thing consists in proving new fact in some > fixed theory, and change only a theory when it fails to prove a fact > for which we have compelling evidences.
How do we know that 0 has a successor though? If 0 x = x and x -0 = x then maybe s(0)=0 or Ez<>s(0)... Can we disprove the idea that a successor to zero does not exist? Sorry, I'm probably not at the minimum level of competence to understand this. -- You received this message because you are subscribed to the Google Groups "Everything List" group. To post to this group, send email to everything-list@googlegroups.com. To unsubscribe from this group, send email to everything-list+unsubscr...@googlegroups.com. For more options, visit this group at http://groups.google.com/group/everything-list?hl=en.
