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 email@example.com.
To unsubscribe from this group, send email to
For more options, visit this group at