Prove that $2+2=4$.

Question

Before you might chastise this quesion, I understand that we all know $2+2=4$. But a while ago I just stumbled across this paper which formally proves that $2+2=4$: http://www.cs.yale.edu/homes/as2446/224.pdf

However, seeing that I had never taken any courses in number theory, I had no exposure to congruence relations, so I have a hard time understanding those areas of the proof. Also, at 1.5 pages, I personally find the proof in the paper to be rather long.

I would write my own proof here (e.g. maybe show that $2+2 \le 4$ and $2+2 \ge 4$ in order to achieve equality?), but I fear that it will be extremely faulty, so I had been wondering for a while:

Are more concise ways to write a formal proof which shows that $2+2=4$, preferably without the use of any congruence relations? I would like to see different ways if possible.

Answer 1

I don't know about more concise, but I will sketch the outline of a simpler proof starting with Peano's Axioms for the natural numbers $(N,0,S)$.

We will construct the function $add: N^2\to N$ such that

$\forall a\in N: add(a,0)=a$

$\forall a,b\in N: add(a,S(b))=S(add(a,b))$

Begin by constructing the set $add$ such that

$\forall a,b,c:[(a,b,c)\in add \iff (a,b,c)\in N^3$

$\land \forall d:[\forall e,f,g: [(e,f,g)\in d\implies (e,f,g)\in N^3]$

$\land \forall e\in N: (e,0,e)\in d$

$\land \forall e,f,g:[(e,f,g)\in d \implies (e,S(f),S(g))\in d]$

$\implies (a,b,c)\in d]]$

Then prove that $add$ is the required function (see full formal proof in DC Proof format, 728 lines).

Then define $1=S(0), 2=S(1), 3=S(2), 4=S(3).$

Then prove, in turn, that $add(2,0)=2, add(2,1)=3, add(2,2)=4$ as required.

Answer 2

Here is an alternative shorter proof, based on the capability of the Prolog programming language doing proofs in Horn clause logic. We first have to massage the definition of addition so that it gets Horn clause form.

I am using these two equality clauses:

$$n+0 = n\quad (1)$$ $$n+m' = (n+m)'\quad (2)$$

Now I introduce a predicate add with the following definition:

$$add(m,n,p) :\Leftrightarrow m+n = p$$

Now observe that in equational logic it is always the case that $A(t) \Leftrightarrow \forall x(t=x \rightarrow A(x))$. We therefore have for (2):

$$n+m' = (n+m)' \Leftrightarrow \forall x(n+m=x \rightarrow n+m'=x')$$

(1) is trivial to translate into a Horn clause. Using the above we can translate (2) into a Horn clause by writing the implication the other direction and using Prolog style implication and s(.) for the successor .':

add(N,0,N).                        /* (1) */
add(N,s(M),s(X)) :- add(N,M,X).    /* (2) */

We can verify 2+2=4 very quickly by running a Prolog system, for example here SWI-Prolog:

Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.25-3-gc3a87c2)
Copyright (c) 1990-2016 University of Amsterdam, VU Amsterdam

?- add(s(s(0)), s(s(0)), s(s(s(s(0))))).
true .

In fact 3 inference steps are needed which are shown in trace mode:

?- trace.
true.

[trace] 3 ?- add(s(s(0)), s(s(0)), s(s(s(s(0))))).
   Call: (7) add(s(s(0)), s(s(0)), s(s(s(s(0))))) ? creep
   Call: (8) add(s(s(0)), s(0), s(s(s(0)))) ? creep
   Call: (9) add(s(s(0)), 0, s(s(0))) ? creep
   Exit: (9) add(s(s(0)), 0, s(s(0))) ? creep
   Exit: (8) add(s(s(0)), s(0), s(s(s(0)))) ? creep
   Exit: (7) add(s(s(0)), s(s(0)), s(s(s(s(0))))) ? creep
true .

Since this is a success Robinson question, not much of the rest of the axioms of Peano are needed, they would be needed to explain failure of a Prolog proof, such as $2+2 ≠ 5$.