Using the Peano axioms, we need to prove that S(0)+S(0)=S(S(0)).

From the definition of +: S(0)+S(0)=S(S(0)+0) Again using the definition of +: S(0)+0=S(0). And we get: S(0)+S(0)=S(S(0))

Q.E.D.

There is also a famous proof by Whitehead and Russell on page 379 of Principia Mathematica: http://quod.lib.umich.edu/cgi/t/text/pageviewer-idx?c=umhist...

Thank you, I didn't know you could prove that!

I believe my disagreement was specifically about this (quoted):

> In principle a computer can correctly recognize 2 apples as

> being 2 apples without knowing anything about addition and

> without being able to recognize 1 apple.

I have a hard time seeing this. If I am not mistaken again, there is no definition of the symbol 2 that does not include addition. The proof above doesn't really prove this either as Peano's axiom rely on the definition of "successor". Successor definition: "a+1 is the successor of a".

http://mathworld.wolfram.com/PeanosAxioms.html

http://mathworld.wolfram.com/Successor.html

See the edit in my reply to tomp. In the Peano axioms, 2 is defined as S(S(0)), not as S(0)+1. The correct way to think about this is to ignore any inclination to give those symbols any "real world" meaning. From the point of view of the formal system - they are just strings, and the only thing we know about them is how to manipulate them to form other strings. Under this perspective, the connection between S(S(0)) and S(0)+1, or in general between S(a) and a+1, is again something which requires proof: S(a) = S(a+0) = a + S(0).

A computer can be given an explicit map between the symbols S(0), S(S(0)), s(S(S(0))), ... and 1,2,3..., so to identify S(S(S(S(S(S(0)))))) with 6 - it wouldn't need to know anything at all about + or about 1.

Edit: also consider the following quote from Wittgenstein's Philosophical Investigations and whether the person described needs to have any concept of 'addition' in order to correctly use numbers: "Now think of the following use of language: I send someone shopping. I give him a slip marked 'five red apples'. He takes the slip to the shopkeeper, who opens the drawer marked 'apples', then he looks up the word 'red' in a table and finds a colour sample opposite it; then he says the series of cardinal numbers--I assume that he knows them by heart--up to the word 'five' and for each number he takes an apple of the same colour as the sample out of the drawer.--It is in this and simlar ways that one operates with words--"But how does he know where and how he is to look up the word 'red' and what he is to do with the word 'five'?" ---Well, I assume that he 'acts' as I have described. Explanations come to an end somewhere.--But what is the meaning of the word 'five'? --No such thing was in question here, only how the word 'five' is used."

This is quite beyond my knowledge, I like the Wittgenstein philosophy, but I would still argue:

You cannot calculate S^(x+1)(0) before the result of S^x(0) is known.

To calculate S^6(0) you start by calculating S(0) ----> It's not possible to "identify S^6(0) with 6" if you haven't calculated S(0) first, because you cannot know S^6(0) at this point.

The computer has a table in memory that tells it S^6(0) = 6 (or equivalently O O O O O O = 6 apples). When it sees a symbol - for example S^6(0) - it searches this table for the same symbol, and then outputs the corresponding number. In no stage of this process does the computer "calculate" anything - it doesn't even need to know that S^5(0)=5 in order to find that S^6(0)=6. In fact S^5 might not even be in the table.

Here is a simple definition of the natural numbers and addition, in Haskell:

    data Nat = Zero | Suc Nat

    plus :: (Nat, Nat) -> Nat
    plus (Zero, y) = y                  -- axiom 1
    plus (Suc x, y) = Suc (plus (x, y)) -- axiom 2

    one = Suc Zero
    two = Suc one

Here is a proof that plus (one, one) = two:

    plus (Suc Zero, Suc Zero)
    = Suc (plus (Zero, Suc Zero))  [by axiom 2]
    = Suc (Suc Zero)               [by axiom 1]

Can you please translate that to mathematics? My request was regarding a formal mathematical proof.

The code I gave translates easily into Agda, a computerized proof checker, and as such more formal than most mathematics. However, here's the same thing in a modernized version of Peano arithmetic. We assume all the usual properties of equality: reflexivity, symmetry, transitivity, and substitution.

    -- Axioms (only 1 and 2 are relevant)
    1. 0 ∈ N
    2. ∀ x∈N. S(x) ∈ N
    3. ∀ x∈N. 0 ≠ S(x)
    4. ∀ x∈N, y∈N. S(x) = S(y) ⊃ x = y
    5. P(0) ∧ (∀ x∈N. P(x) ⊃ P(S(x))) ⊃ ∀ x∈N. P(x)

    -- Definition of addition
    6. ∀ a∈N. a + 0 = a
    7. ∀ a,b ∈ N. a + S(b) = S(a+b)

    -- Proof that S(0) + S(0) = S(S(0))
    9. S(0) ∈ N                     [from 2 and 1]
    10. S(0) + S(0) = S(S(0) + 0)   [from 7 and 9]
    11. S(0) + 0 = S(0)             [from 6 and 9]
    12. S(S(0) + 0) = S(S(0))       [substitution of equals, from 11]
    13. S(0) + S(0) = S(S(0))       [transitivity from 10 and 12]

Edit: Ah, I see I was beaten to it by pavelrub.