# Re: Math Question

```
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