On 31 Jul 2011, at 17:08, Craig Weinberg wrote:
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?
No. 0 is primitive term, and the language allows the term s(t) for all
term t, so you have the terms 0, s(0), s(s(0)), etc.
The rest follows from the axioms For all x 0 ≠ s(x), s(x) = s(y) -> x
= y (so that all numbers have only one successor. So you can, prove,
even without induction, that 0 has a unique successor, different from
itself.
Sorry, I'm probably not at the
minimum level of competence to understand this.
I look on the net, but I see errors (Wolfram's definition is Dedekind
Arithmetic!)? On wiki, the definition of Peano arithmetic seems
correct. You need to study some elementary textbook in mathematical
logic. Most presentation assumes you know what is first order
predicate logic. You can google on those terms. There are good books,
but it is a bit involved subject and ask for some works. Peano
Arithmetic is the simplest example of Löbian theory or machines or
belief system. It is very powerful. You light take time to find an
arithmetical proposition that you can prove to be true and that she
can't, especially without using the technics for doing that. Most
interesting theorem in usual (non Logic) mathematics can be prove in
or by PA. And PA, like all Löbian machine, can prove its own Gödel
theorem (if "I" am consistent then "I" cannot prove that "I "am
consistent). The "I" is a 3-I.
Bruno
--
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
.
http://iridia.ulb.ac.be/~marchal/
--
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.
