Peano Addition • 1+1=2 proved via Resolution

Formalize addition with successor and show a canonical entailment

We use a standard Peano-style signature with a constant and a unary function:

// Symbols:
//   0            // zero
//   s(x)         // successor of x
// Predicate:
//   add(x, y, z) // "x + y = z"
//
// Axioms for addition (Horn clauses):
// A1: add(x, 0, x).
// A2: add(x, y, z) -> add(x, s(y), s(z)).

Goal (ground instance to prove by Resolution): add(s(0), s(0), s(s(0))) — i.e., 1 + 1 = 2.

Entailed. Using the axioms A1–A2 and refuting the negation of the goal with Resolution derives the empty clause.

Resolution justification (clausal refutation)

1. Clausal form (already Horn): C1: add(X, 0, X) C2: ¬add(X, Y, Z) ∨ add(X, s(Y), s(Z))
2. Negate the goal and add it: N0: ¬add(s(0), s(0), s(s(0))).
3. Resolve N0 with C2 (unifier: X:=s(0), Y:=0, Z:=s(0)) to obtain R1: ¬add(s(0), 0, s(0)).
4. Resolve R1 with C1 (unifier: X:=s(0)) to get ⟂ (empty clause).
5. Therefore add(s(0), s(0), s(s(0))) follows from A1–A2.

Concrete computation: 1 + 1

Randomized small sums

Test x,y ∈ {0..3} and compare the logical add with JavaScript’s +.

Exhaustive tiny domain (0..2)

Verify all pairs (x,y) map to x+y as expected.

Right identity

Confirm add(x, 0) = x for sampled x.

Step rule matches the axiom

Check that add(x, s(y)) = s(add(x, y)) for random x,y.

Your data (CSV)

Provide “X: 2” and “Y: 3”. We compute X + Y as a Peano term and as a number.

Automated Resolution trace (for 1+1=2)