7. Peano Arithmetic in Lambda Calculus

7. Peano Arithmetic in Lambda Calculus#

Goal. Rebuild the foundations of Peano arithmetic using Church numerals and prove simple number-theoretic facts.

You will learn

How Church numerals model Peano-style arithmetic operations
How to define mod and divisibility predicates via recursion (Z + IF_THUNK)
How to reason about parity and simple congruences in a functional style
How to separate proof sketches (math) from finite checks (code)
How these results set up the induction chapters (8 and 9)

Roadmap#

Recall the Peano viewpoint and fix canonical Church arithmetic operators.
Define modulo and divisibility in Church style.
Work through parity and congruence examples (including mod 2 and mod 8).
Practice by writing and checking small arithmetic identities.
Transition to fully general induction proofs in Chapters 8 and 9.

Convention (Proof vs Check)

In this chapter, theorem text gives the mathematical proof idea, while code loops are bounded computational checks. Fully general induction objects are given in Chapters 8 and 9.

Definition (Peano Axioms, Informal)

The natural numbers are generated from:

0 is a natural number.
If n is a natural number, so is S(n) (successor).
0 is not the successor of any number.
If S(n) = S(m) then n = m (injectivity of successor).
(Induction) If P(0) and P(n) → P(S(n)), then P(n) holds for all n.

We model these axioms using Church numerals, where 0 and S are lambda terms.

Remark (Why IF_THUNK Again?)

We reuse IF_THUNK because recursive definitions like mod would otherwise evaluate both branches eagerly and diverge. Wrapping branches as lambda: ... keeps the recursion safe.

from pathlib import Path
import sys

book_root = Path.cwd()
if not (book_root / 'church_core.py').exists():
    book_root = book_root.parent
if str(book_root) not in sys.path:
    sys.path.insert(0, str(book_root))

from church_core import (
    TRUE,
    FALSE,
    IF,
    IF_THUNK,
    AND,
    to_bool,
    church,
    from_int,
    to_int,
    succ,
    add,
    mul,
    pair,
    fst,
    snd,
    pred,
    sub,
    is_zero,
    leq_church,
    eq_church,
    Z,
)

# Handy numerals for examples
zero = church(0)
one = church(1)
two = church(2)
three = church(3)
eight = church(8)

# Naming convenience in this chapter
leq = leq_church
eq = eq_church

Lemma (Basic Laws)

The following are valid for Church numerals and correspond to Peano arithmetic.

n + 0 = n
n + S(m) = S(n + m)
n * 0 = 0
n * S(m) = n * m + n

Remark

The identities above are proved fully in the induction chapter: Mathematical Induction.

We can check these laws computationally for a small range as a sanity check.

def assert_equal(a, b):
    return to_int(a) == to_int(b)

for n in range(5):
    n_ch = from_int(n)
    assert assert_equal(add(n_ch)(zero), n_ch)
    assert assert_equal(mul(n_ch)(zero), zero)

print('Basic laws verified for n < 5')

Basic laws verified for n < 5

Theorem (Divisibility Example)

For every natural number n, the number (2n + 1)^2 - 1 is divisible by 8.

Proof sketch. (2n + 1)^2 - 1 = 4n^2 + 4n = 4n(n+1). One of n and n+1 is even, so n(n+1) = 2k for some k. Therefore (2n + 1)^2 - 1 = 4 * 2k = 8k, which is divisible by 8.

We’ll verify this with Church numerals by constructing a divisible_by_8 predicate.

mod = Z(
    lambda mod: (
        lambda n: (
            lambda m: IF_THUNK(leq(n)(pred(m)))(lambda: n)(lambda: mod(sub(n)(m))(m))
        )
    )
)

divisible_by_8 = lambda n: is_zero(mod(n)(eight))

double = lambda n: mul(two)(n)
square = lambda n: mul(n)(n)
expr = lambda n: sub(square(add(double(n))(one)))(one)

for n in range(10):
    n_ch = from_int(n)
    val = expr(n_ch)
    print(n, to_int(val), to_bool(divisible_by_8(val)))

0 True
8 True
24 True
48 True
80 True
120 True
168 True
224 True
288 True

9 360 True

Example (Evenness of n(n+1))

Another nice lambda-calculus proof target: n(n+1) is even. In Church encodings, this means is_even(mul(n)(succ(n))) should return TRUE.

is_even = lambda n: is_zero(mod(n)(two))

for n in range(8):
    n_ch = from_int(n)
    val = mul(n_ch)(succ(n_ch))
    print(n, to_int(val), to_bool(is_even(val)))

0 True
2 True
6 True
12 True
20 True
30 True
42 True
56 True

Congruence Examples (Functional Style)#

We now add several congruence proofs with full functional detail. We use the standard definition:

\[a \equiv b \pmod m \iff m \mid (a-b).\]

In Church numerals, we compute congruence by comparing remainders.

Definition (Congruence)

We say \(a\) is congruent to \(b\) modulo \(m\) if

\[\operatorname{mod}(a,m)=\operatorname{mod}(b,m).\]

Equivalently, \(m \mid (a-b)\).

# Congruence helpers
congruent = lambda a: (lambda b: (lambda m: eq(mod(a)(m))(mod(b)(m))))
divisible_by = lambda n: (lambda m: is_zero(mod(n)(m)))

four = from_int(4)

Lemma (Evenness of \(n(n+1)\))

For all \(n\), \(n(n+1)\) is divisible by \(2\).

Proof (functional style). One of \(n\) and \(n+1\) is even. If \(n\) is even, then \(n(n+1)\) is even. If \(n\) is odd, then \(n+1\) is even, so \(n(n+1)\) is even again. We verify this by checking that the remainder modulo \(2\) is zero.

for n in range(8):
    N = from_int(n)
    val = mul(N)(succ(N))
    print(n, to_int(val), to_bool(divisible_by(val)(two)))

0 True
2 True
6 True
12 True
20 True
30 True
42 True
56 True

Lemma (Parity of Squares)

For all \(n\), \(n^2 \equiv n \pmod 2\).

Proof (functional style). If \(n\) is even, then \(n=2k\) and \(n^2=4k^2\), so both are congruent to \(0\) modulo \(2\). If \(n\) is odd, then \(n=2k+1\) and \(n^2=4k(k+1)+1\), so both are congruent to \(1\) modulo \(2\). Hence \(n^2 \equiv n \pmod 2\).

for n in range(8):
    N = from_int(n)
    left = square(N)
    right = N
    ok = to_bool(congruent(left)(right)(two))
    print(n, to_int(left), to_int(right), ok)

0 0 True
1 1 True
4 2 True
9 3 True
16 4 True
25 5 True
36 6 True
49 7 True

Lemma (Square of an Even Number)

For all \(n\), \((2n)^2 \equiv 0 \pmod 4\).

Proof (functional style). \((2n)^2 = 4n^2\), so the remainder modulo \(4\) is zero.

for n in range(8):
    N = from_int(n)
    val = square(double(N))
    ok = to_bool(congruent(val)(zero)(four))
    print(n, to_int(val), ok)

0 True
4 True
16 True
36 True
64 True
100 True
144 True
196 True

Lemma (Odd Square Mod 8)

For all \(n\), \((2n+1)^2 \equiv 1 \pmod 8\).

Proof (functional style). \((2n+1)^2 - 1 = 4n(n+1)\). One of \(n\) and \(n+1\) is even, so \(4n(n+1)\) is divisible by \(8\). Hence \((2n+1)^2 \equiv 1 \pmod 8\).

for n in range(8):
    N = from_int(n)
    val = square(add(double(N))(one))
    ok = to_bool(congruent(val)(one)(eight))
    print(n, to_int(val), ok)

1 True
9 True
25 True
49 True
81 True
121 True
169 True
225 True

Exercise

Define is_odd and show that is_odd(n) = NOT(is_even(n)).
Prove (by computation) that n + m = m + n for small n, m.
Define pow and verify (2n)^2 = 4n^2 for small n.
Define odd_square_minus_one(n) = (2n+1)^2 - 1 and verify it is divisible by 8 for small n. See solution: Exercise 7 (Peano Arithmetic)

Summary#

Church arithmetic supports a Peano-like development of basic number theory.
Recursion (via Z) and lazy branching (IF_THUNK) enable definitions like modulo.
Many congruence statements have short algebraic proofs and can be validated by finite computation.
The crucial upgrade is generality: Chapters 8 and 9 develop induction-based proofs that go beyond bounded checks.
Next: formal induction patterns and proof traces for Church arithmetic identities (Chapter 8).