Prove that $2+2=4$.

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.

• I see from the paper that it is from 2010. I would conjecture April 1, 2010. – André Nicolas Jun 21 '14 at 5:41
• A formal proof for $2+2=4$ can be given (I used it as an exercise in a course once). The sought after solution depended on the definitions of: "$2$", "$4$" and "$+$" as they are commonly given in the context of Peano axioms. – Jyrki Lahtonen Jun 21 '14 at 6:00
• It depends as @JyrkiLahtonen says on definitions. The associative law makes sense of the equation $(1+1)+(1+1)=1+1+1+1$ which can be formulated in any ring. What you call the components varies - in characteristic $2$ this is normally written $0+0=0$, in characteristic $3$ it is $2+2=1$ and characteristic $4$ we get $2+2=0$ – Mark Bennet Jun 21 '14 at 6:55
• If you go to the root of the website, this article belongs to "recreational mathmeatics". – Taladris Jun 22 '14 at 5:54
• The so-called proof in your paper makes use of Fermat’s Little Theorem; this theorem regards prime numbers which definition involves division, and division needs multiplication. Then the issue is : are we able to define multiplication between natural numbers without having proved the basic properties of addition between them ? – Mauro ALLEGRANZA Jun 22 '14 at 9:07

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.

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) */


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

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$.