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.

##
Advertising

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.