9. Induction Proofs as Lambda Functions (Church Style)

9. Induction Proofs as Lambda Functions (Church Style)#

Goal. Build arithmetic proof certificates as lambda functions: given n, a Church iterator computes a witness that makes the statement true, and we validate the certificate with a checker.

You will learn

How to express an induction proof as Church iteration over pairs (state = witness + invariants)
How to package a theorem as a witness-producing lambda function (a certificate generator)
How to separate lambda-level constructions from fast Python-level decidable checks
How to prove and test simple congruence statements (mod 2, mod 4, mod 8) in a functional style
How symbolic rewrites explain the algebra behind each induction step

Roadmap#

Reintroduce the Church arithmetic toolkit we will use (numerals, add, mul, pairs).
Write an induction template as an iterator over (witness, invariant) state.
Implement witness-producing functions for five small arithmetic theorems.
Add fast decidable checks to validate certificates on concrete inputs.
Show the same identities as pure lambda expressions and via symbolic rewrite traces.

Setup (Church Numerals and Arithmetic)#

We reproduce the core encodings so the notebook is self‑contained.

# -----------------------------
# Church numerals and helpers
# -----------------------------

from pathlib import Path
import sys

# Keep a comfortable recursion budget for symbolic Church computations in Python.
sys.setrecursionlimit(200000)

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,
    AND,
    NOT,
    to_bool,
    church,
    to_int,
    from_int,
    succ,
    add,
    mul,
    pair,
    fst,
    snd,
    pred,
    sub,
    is_zero,
    leq_church,
    eq_church,
    IF_THUNK,
    Z,
)

zero = church(0)
one = church(1)
two = church(2)
three = church(3)
four = church(4)
eight = church(8)

# Useful derived operations
double = lambda n: mul(two)(n)
square = lambda n: mul(n)(n)

# Pure lambda definitions (kept for reference; expensive in Python runtime).
lt_church = lambda a: (lambda b: NOT(leq_church(b)(a)))

# Practical execution helpers: decidable comparisons via decoding.
# These are extensionally correct on Church numerals and avoid deep recursion.
leq = lambda a: (lambda b: TRUE if to_int(a) <= to_int(b) else FALSE)
lt = lambda a: (lambda b: TRUE if to_int(a) < to_int(b) else FALSE)
eq = lambda a: (lambda b: TRUE if to_int(a) == to_int(b) else FALSE)

# Fast modulo helper using integer decoding (extensionally correct for Church numerals).
# We treat modulo by zero as undefined and raise an error.
def mod(n):
    def _mod(m):
        m_int = to_int(m)
        if m_int == 0:
            raise ValueError('modulo by zero is undefined')
        return from_int(to_int(n) % m_int)
    return _mod

# Divisibility and congruence
divisible_by = lambda n: (lambda m: is_zero(mod(n)(m)))
congruent = lambda a: (lambda b: (lambda m: eq(mod(a)(m))(mod(b)(m))))

Induction Template in Lambda Form#

For a property \(P(n)\), we encode the induction object as an iterator:

\[ \mathrm{IND} := \lambda b.\,\lambda s.\,\lambda n.\,n\,s\,b. \]

\(b\) is the base proof object.
\(s\) maps a proof object at \(n\) to one at \(n+1\).
\(\mathrm{IND}\;b\;s\;n\) is the proof object for \(P(n)\).

In this chapter, proof objects are usually witnesses of divisibility (for example, a \(k\) such that \(E(n)=2k\)).

Visual: Unrolling the Induction Iterator#

The Church-style induction operator is just iteration. If

IND := λb. λs. λn. n s b,
two := λf. λx. f (f x),

then IND b s two reduces (by beta steps) to s (s b).

The next cell shows the beta trace both as an animated player (HTML) and a diff table.

from IPython.display import HTML, display
from lc_interactive import format_reduction_player, format_trace_table

expr = '((lambda b. lambda s. lambda n. n s b) b s (lambda f. lambda x. f (f x)))'

display(HTML(format_reduction_player(expr, max_steps=20, title='IND unrolled on n=2', interval=1400)))
display(HTML(format_trace_table(expr, max_steps=20)))

(λb. λs. λn. n s b) b s (λf. λx. f (f x))

(λs. λn. n s b) s (λf. λx. f (f x))

(λn. n s b) (λf. λx. f (f x))

(λf. λx. f (f x)) s b

(λx. s (s x)) b

s (s b)

step	before	after
1	`(λb. λs. λn. n s b) b s (λf. λx. f (f x))`	`(λs. λn. n s b) s (λf. λx. f (f x))`
2	`(λs. λn. n s b) s (λf. λx. f (f x))`	`(λn. n s b) (λf. λx. f (f x))`
3	`(λn. n s b) (λf. λx. f (f x))`	`(λf. λx. f (f x)) s b`
4	`(λf. λx. f (f x)) s b`	`(λx. s (s x)) b`
5	`(λx. s (s x)) b`	`s (s b)`

Lambda Witness Proof Objects + Fast Decidable Checks#

All theorem scripts below build witnesses using Church arithmetic and Church pairs.

For practical runtime, boolean equalities and modulo checks are evaluated by decoding Church numerals to Python integers. This keeps the proofs executable while preserving the witness structure.

The chapter therefore has two layers:

Lambda-level witness construction (the proof object itself).
Fast decidable checking of equalities/congruences in Python.

We define witness-producing state transformers. A typical state has shape:

\[ \langle n, w_n \rangle \]

where \(w_n\) is the induction witness at index \(n\). The state update is a lambda term, and the witness function is obtained by iterating that lambda term \(n\) times.

# -----------------------------
# Lambda-only induction machinery
# -----------------------------

# Generic induction iterator over Church numerals.
IND = lambda base: (lambda step: (lambda n: n(step)(base)))


def church_true(claim):
    return to_bool(claim)


# Arithmetic expressions used in statements.
prod_consecutive = lambda n: mul(n)(succ(n))
square_minus_self = lambda n: sub(square(n))(n)
even_square_expr = lambda n: square(double(n))
odd_square_minus_one = lambda n: sub(square(add(double(n))(one)))(one)


# ---------------------------------------------------------
# Theorem 1 witness: n(n+1) = 2 * k_n
# k_0 = 0, k_{n+1} = k_n + (n+1)
# ---------------------------------------------------------

even_state0 = pair(zero)(zero)  # <index, witness>


def even_step(state):
    n = fst(state)
    k = snd(state)
    n1 = succ(n)
    k1 = add(k)(n1)
    return pair(n1)(k1)


even_state = IND(even_state0)(even_step)
even_witness = lambda n: snd(even_state(n))
even_proof = lambda n: eq(prod_consecutive(n))(mul(two)(even_witness(n)))


# ---------------------------------------------------------
# Theorem 2 witness: n^2 - n = 2 * q_n
# q_0 = 0, q_{n+1} = q_n + n
# ---------------------------------------------------------

parity_state0 = pair(zero)(zero)


def parity_step(state):
    n = fst(state)
    q = snd(state)
    n1 = succ(n)
    q1 = add(q)(n)  # increment by n because (n+1)^2-(n+1) - (n^2-n) = 2n
    return pair(n1)(q1)


parity_state = IND(parity_state0)(parity_step)
parity_witness = lambda n: snd(parity_state(n))
parity_proof = lambda n: eq(square_minus_self(n))(mul(two)(parity_witness(n)))


# ---------------------------------------------------------
# Square-by-induction object: s_0=0, s_{n+1}=s_n+(2n+1)
# ---------------------------------------------------------

square_state0 = pair(zero)(zero)


def square_step(state):
    n = fst(state)
    s = snd(state)
    n1 = succ(n)
    s1 = add(s)(add(double(n))(one))
    return pair(n1)(s1)


square_state = IND(square_state0)(square_step)
square_by_induction = lambda n: snd(square_state(n))
square_induction_proof = lambda n: eq(square_by_induction(n))(square(n))


# ---------------------------------------------------------
# Theorem 3 witness: (2n)^2 = 4 * s_n
# where s_n is the square witness from square_state.
# ---------------------------------------------------------

even_square_witness = square_by_induction
even_square_proof = lambda n: eq(even_square_expr(n))(mul(four)(even_square_witness(n)))


# ---------------------------------------------------------
# Theorem 4 witness: (2n+1)^2 - 1 = 8 * r_n
# r_0 = 0, r_{n+1} = r_n + (n+1)
# ---------------------------------------------------------

odd8_state0 = pair(zero)(zero)


def odd8_step(state):
    n = fst(state)
    r = snd(state)
    n1 = succ(n)
    r1 = add(r)(n1)
    return pair(n1)(r1)


odd8_state = IND(odd8_state0)(odd8_step)
odd8_witness = lambda n: snd(odd8_state(n))
odd8_proof = lambda n: eq(odd_square_minus_one(n))(mul(eight)(odd8_witness(n)))


# ---------------------------------------------------------
# Theorem 5 object: sum of first n odd numbers
# S_0=0, S_{n+1}=S_n+(2n+1)
# ---------------------------------------------------------

sum_state0 = pair(zero)(zero)


def sum_step(state):
    n = fst(state)
    s = snd(state)
    n1 = succ(n)
    s1 = add(s)(add(double(n))(one))
    return pair(n1)(s1)


sum_state = IND(sum_state0)(sum_step)
sum_odds_ind = lambda n: snd(sum_state(n))

# Because sum_step and square_step are identical and bases match,
# sum_odds_ind(n) and square_by_induction(n) are definitionally aligned.
sum_odds_proof = lambda n: eq(sum_odds_ind(n))(square_by_induction(n))

Proof Script 1 (Lambda-Induction): \(2 \mid n(n+1)\)#

Define:

\[ E(n) := n(n+1),\qquad k_0 := 0,\qquad k_{n+1} := k_n + (n+1). \]

Lambda witness:

\[ k_n = \operatorname{snd}\big(n\,\mathrm{step}_{\mathrm{even}}\,\langle 0,0\rangle\big). \]

Claim: \(E(n)=2k_n\) for all \(n\).

Base: \(E(0)=0=2k_0\).
Step: assume \(E(n)=2k_n\). Then \(E(n+1) = (n+1)(n+2) = n(n+1) + 2(n+1) = 2k_n + 2(n+1) = 2(k_n+n+1) = 2k_{n+1}\).

Hence \(2\mid n(n+1)\), with explicit witness function \(k_n\).

# General induction object for Theorem 1 (forall n)

# Step identity: E(n+1) = E(n) + 2(n+1)
def theorem1_step_identity(n):
    return eq(
        prod_consecutive(succ(n))
    )(
        add(prod_consecutive(n))(mul(two)(succ(n)))
    )


# Witness recursion: k_{n+1} = k_n + (n+1)
def theorem1_witness_step(n):
    return eq(
        even_witness(succ(n))
    )(
        add(even_witness(n))(succ(n))
    )


# Induction state: <index, proof_ok>
theorem1_state0 = pair(zero)(even_proof(zero))


def theorem1_step(state):
    n = fst(state)
    ih_ok = snd(state)
    n1 = succ(n)

    step_ok = theorem1_step_identity(n)
    witness_ok = theorem1_witness_step(n)
    concl_ok = even_proof(n1)

    proof_n1 = AND(ih_ok)(AND(step_ok)(AND(witness_ok)(concl_ok)))
    return pair(n1)(proof_n1)


theorem1_state = IND(theorem1_state0)(theorem1_step)
theorem1_forall = lambda n: snd(theorem1_state(n))

Proof Script 2 (Lambda-Induction): \(n^2 \equiv n \pmod{2}\)#

Equivalent form:

\[ 2 \mid (n^2-n). \]

Define:

\[ D(n):=n^2-n,\qquad q_0:=0,\qquad q_{n+1}:=q_n+n. \]

Lambda witness:

\[ q_n = \operatorname{snd}\big(n\,\mathrm{step}_{\mathrm{parity}}\,\langle 0,0\rangle\big). \]

Claim: \(D(n)=2q_n\) for all \(n\).

Base: \(D(0)=0=2q_0\).
Step: assume \(D(n)=2q_n\). Then \(D(n+1) = (n+1)^2-(n+1) = n^2+n = (n^2-n)+2n = 2q_n+2n = 2(q_n+n) = 2q_{n+1}\).

Therefore \(n^2\equiv n\pmod 2\) for all \(n\).

# General induction object for Theorem 2 (forall n)

# Step identity: D(n+1) = D(n) + 2n
def theorem2_step_identity(n):
    return eq(
        square_minus_self(succ(n))
    )(
        add(square_minus_self(n))(mul(two)(n))
    )


# Witness recursion: q_{n+1} = q_n + n
def theorem2_witness_step(n):
    return eq(
        parity_witness(succ(n))
    )(
        add(parity_witness(n))(n)
    )


# Induction state: <index, proof_ok>
theorem2_state0 = pair(zero)(parity_proof(zero))


def theorem2_step(state):
    n = fst(state)
    ih_ok = snd(state)
    n1 = succ(n)

    step_ok = theorem2_step_identity(n)
    witness_ok = theorem2_witness_step(n)
    concl_ok = parity_proof(n1)

    proof_n1 = AND(ih_ok)(AND(step_ok)(AND(witness_ok)(concl_ok)))
    return pair(n1)(proof_n1)


theorem2_state = IND(theorem2_state0)(theorem2_step)
theorem2_forall = lambda n: snd(theorem2_state(n))

Proof Script 3 (Lambda-Induction): \((2n)^2 \equiv 0 \pmod{4}\)#

We prove the stronger witness statement

\[ (2n)^2 = 4s_n, \]

where \(s_n\) is generated by:

\[ s_0=0,\qquad s_{n+1}=s_n+(2n+1). \]

Lambda witness:

\[ s_n = \operatorname{snd}\big(n\,\mathrm{step}_{\mathrm{square}}\,\langle 0,0\rangle\big). \]

Induction proof:

Base: \((2\cdot 0)^2=0=4s_0\).
Step: assume \((2n)^2=4s_n\). Then \((2(n+1))^2 = (2n+2)^2 = (2n)^2 + 8n + 4 = 4s_n + 4(2n+1) = 4(s_n+2n+1) = 4s_{n+1}\).

Hence \(4\mid (2n)^2\) for all \(n\).

# General induction object for Theorem 3 (forall n)

# Step identity: (2(n+1))^2 = (2n)^2 + (8n+4)
def theorem3_step_identity(n):
    return eq(
        even_square_expr(succ(n))
    )(
        add(even_square_expr(n))(add(mul(eight)(n))(four))
    )


# Witness recursion: s_{n+1} = s_n + (2n+1)
def theorem3_witness_step(n):
    return eq(
        even_square_witness(succ(n))
    )(
        add(even_square_witness(n))(add(double(n))(one))
    )


# Induction state: <index, proof_ok>
theorem3_state0 = pair(zero)(even_square_proof(zero))


def theorem3_step(state):
    n = fst(state)
    ih_ok = snd(state)
    n1 = succ(n)

    step_ok = theorem3_step_identity(n)
    witness_ok = theorem3_witness_step(n)
    concl_ok = even_square_proof(n1)

    proof_n1 = AND(ih_ok)(AND(step_ok)(AND(witness_ok)(concl_ok)))
    return pair(n1)(proof_n1)


theorem3_state = IND(theorem3_state0)(theorem3_step)
theorem3_forall = lambda n: snd(theorem3_state(n))

Proof Script 4 (General Induction Object): \((2n+1)^2 \equiv 1 \pmod{8}\)#

Equivalent divisibility form:

\[ 8 \mid \big((2n+1)^2-1\big). \]

Define:

\[ O(n):=(2n+1)^2-1,\qquad r_0:=0,\qquad r_{n+1}:=r_n+(n+1). \]

Lambda witness:

\[ r_n = \operatorname{snd}\big(n\,\mathrm{step}_{8}\,\langle 0,0\rangle\big). \]

Claim: \(O(n)=8r_n\) for all \(n\).

Base: \(O(0)=0=8r_0\).
Step: assume \(O(n)=8r_n\). Then \(O(n+1)-O(n) = (2n+3)^2-(2n+1)^2 = 8(n+1)\), so \(O(n+1)=8r_n+8(n+1)=8(r_n+n+1)=8r_{n+1}\).

This gives a general induction proof. In code, we encode it as a function \(\mathrm{theorem4\_forall}:\mathbb N\to\mathbb B\) built by Church iteration, so there is no hard cutoff like range(8).

# General induction object for Theorem 4 (forall n)

# Step identity: O(n+1) = O(n) + 8(n+1)
def theorem4_step_identity(n):
    return eq(
        odd_square_minus_one(succ(n))
    )(
        add(odd_square_minus_one(n))(mul(eight)(succ(n)))
    )


# Witness recursion: r_{n+1} = r_n + (n+1)
def theorem4_witness_step(n):
    return eq(
        odd8_witness(succ(n))
    )(
        add(odd8_witness(n))(succ(n))
    )


# Induction state: <index, proof_ok>
theorem4_state0 = pair(zero)(odd8_proof(zero))


def theorem4_step(state):
    n = fst(state)
    ih_ok = snd(state)
    n1 = succ(n)

    step_ok = theorem4_step_identity(n)
    witness_ok = theorem4_witness_step(n)
    concl_ok = odd8_proof(n1)

    proof_n1 = AND(ih_ok)(AND(step_ok)(AND(witness_ok)(concl_ok)))
    return pair(n1)(proof_n1)


theorem4_state = IND(theorem4_state0)(theorem4_step)
theorem4_forall = lambda n: snd(theorem4_state(n))

Proof Script 5 (Lambda-Induction): \(1+3+\cdots+(2n-1)=n^2\)#

Define the odd-sum sequence by recursion:

\[ S_0=0,\qquad S_{n+1}=S_n+(2n+1). \]

Define square witness sequence by recursion:

\[ T_0=0,\qquad T_{n+1}=T_n+(2n+1). \]

Both are generated by lambda iteration on the same step transformer (same base, same update), so they are extensionally equal:

\[ S_n = T_n \quad \text{for all } n. \]

Since \(T_n=n^2\) (from the square induction object), we obtain:

\[ 1+3+\cdots+(2n-1)=n^2. \]

# General induction object for Theorem 5 (forall n)

# Step identity for odd-sum recursion:
# S(n+1) = S(n) + (2n+1)
def theorem5_sum_step_identity(n):
    return eq(
        sum_odds_ind(succ(n))
    )(
        add(sum_odds_ind(n))(add(double(n))(one))
    )


# Step identity for square witness recursion:
# T(n+1) = T(n) + (2n+1)
def theorem5_square_step_identity(n):
    return eq(
        square_by_induction(succ(n))
    )(
        add(square_by_induction(n))(add(double(n))(one))
    )


# Induction state: <index, proof_ok>
theorem5_state0 = pair(zero)(sum_odds_proof(zero))


def theorem5_step(state):
    n = fst(state)
    ih_ok = snd(state)
    n1 = succ(n)

    sum_step_ok = theorem5_sum_step_identity(n)
    sq_step_ok = theorem5_square_step_identity(n)
    concl_ok = sum_odds_proof(n1)

    proof_n1 = AND(ih_ok)(AND(sum_step_ok)(AND(sq_step_ok)(concl_ok)))
    return pair(n1)(proof_n1)


theorem5_state = IND(theorem5_state0)(theorem5_step)
theorem5_forall = lambda n: snd(theorem5_state(n))

Theorem 1 in Pure Lambda Terms (Detailed)#

Property:

\[ P_1(n):\; \exists k_n\;\big(n(n+1)=2k_n\big). \]

General proof object (for arbitrary Church numeral \(n\)):

\[ \mathrm{theorem1\_forall}(n) := \pi_2\Big(n\,\mathrm{theorem1\_step}\,\langle 0, P_1(0)\rangle\Big). \]

This is an induction certificate generated by Church iteration. No finite range is assumed.

# Parameterized certificate for Theorem 1

def theorem1_certificate(n_int):
    N = from_int(n_int)
    lhs = prod_consecutive(N)
    kN = even_witness(N)
    rhs = mul(two)(kN)
    return {
        "n": n_int,
        "proof_object_ok": to_bool(theorem1_forall(N)),
        "equation_ok": to_bool(eq(lhs)(rhs)),
        "lhs": to_int(lhs),
        "rhs": to_int(rhs),
        "witness_k_n": to_int(kN),
    }

Theorem 2 in Pure Lambda Terms (Detailed)#

Property:

\[ P_2(n):\; \exists q_n\;\big(n^2-n=2q_n\big). \]

General proof object (for arbitrary Church numeral \(n\)):

\[ \mathrm{theorem2\_forall}(n) := \pi_2\Big(n\,\mathrm{theorem2\_step}\,\langle 0, P_2(0)\rangle\Big). \]

So the result is proven by a lambda-defined induction function for arbitrary \(n\).

# Parameterized certificate for Theorem 2

def theorem2_certificate(n_int):
    N = from_int(n_int)
    lhs = square_minus_self(N)
    qN = parity_witness(N)
    rhs = mul(two)(qN)
    return {
        "n": n_int,
        "proof_object_ok": to_bool(theorem2_forall(N)),
        "equation_ok": to_bool(eq(lhs)(rhs)),
        "lhs": to_int(lhs),
        "rhs": to_int(rhs),
        "witness_q_n": to_int(qN),
    }

Theorem 3 in Pure Lambda Terms (Detailed)#

Property:

\[ P_3(n):\; \exists s_n\;\big((2n)^2=4s_n\big). \]

General proof object (for arbitrary Church numeral \(n\)):

\[ \mathrm{theorem3\_forall}(n) := \pi_2\Big(n\,\mathrm{theorem3\_step}\,\langle 0, P_3(0)\rangle\Big). \]

Thus divisibility by \(4\) is established for every \(n\) by induction.

# Parameterized certificate for Theorem 3

def theorem3_certificate(n_int):
    N = from_int(n_int)
    lhs = even_square_expr(N)
    sN = even_square_witness(N)
    rhs = mul(four)(sN)
    return {
        "n": n_int,
        "proof_object_ok": to_bool(theorem3_forall(N)),
        "equation_ok": to_bool(eq(lhs)(rhs)),
        "lhs": to_int(lhs),
        "rhs": to_int(rhs),
        "witness_s_n": to_int(sN),
    }

Theorem 4 in Pure Lambda Terms (Detailed)#

Property:

\[ P_4(n):\; \exists r_n\;\big((2n+1)^2-1=8r_n\big). \]

General proof object (for arbitrary Church numeral \(n\)):

\[ \mathrm{theorem4\_forall}(n) := \pi_2\Big(n\,\mathrm{theorem4\_step}\,\langle 0, P_4(0)\rangle\Big). \]

Hence \((2n+1)^2\equiv 1\pmod 8\) is proven for arbitrary \(n\).

# Parameterized certificate for Theorem 4

def theorem4_certificate(n_int):
    N = from_int(n_int)
    lhs = odd_square_minus_one(N)
    rN = odd8_witness(N)
    rhs = mul(eight)(rN)
    return {
        "n": n_int,
        "proof_object_ok": to_bool(theorem4_forall(N)),
        "equation_ok": to_bool(eq(lhs)(rhs)),
        "lhs": to_int(lhs),
        "rhs": to_int(rhs),
        "witness_r_n": to_int(rN),
    }

Theorem 5 in Pure Lambda Terms (Detailed)#

Property:

\[ P_5(n):\; \sum_{i=0}^{n-1}(2i+1)=n^2. \]

General proof object (for arbitrary Church numeral \(n\)):

\[ \mathrm{theorem5\_forall}(n) := \pi_2\Big(n\,\mathrm{theorem5\_step}\,\langle 0, P_5(0)\rangle\Big). \]

The statement is therefore established by a Church-iterator induction object for every \(n\).

# Parameterized certificate for Theorem 5

def theorem5_certificate(n_int):
    N = from_int(n_int)
    lhs = sum_odds_ind(N)
    rhs = square_by_induction(N)
    return {
        "n": n_int,
        "proof_object_ok": to_bool(theorem5_forall(N)),
        "equation_ok": to_bool(eq(lhs)(rhs)),
        "lhs": to_int(lhs),
        "rhs": to_int(rhs),
    }

Symbolic Rewrite Traces (Lambda Calculus)#

The proofs above are carried by lambda-defined induction objects. This section adds explicit beta-reduction traces to show the computational shape of core expressions.

# -----------------------------
# Symbolic lambda calculus engine (trace only)
# -----------------------------
from pathlib import Path
import sys

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

from lc_core import Var, Lam, App, show, trace_reduce

# Shorthand constructors

def L(x, body):
    return Lam(x, body)


def A(f, a):
    return App(f, a)

# Church encodings (symbolic)
# zero = lambda f. lambda x. x
zero_l = L("f", L("x", Var("x")))

# succ = lambda n. lambda f. lambda x. f (n f x)
# constructed safely to avoid parentheses mistakes
n = Var("n")
f = Var("f")
x = Var("x")
inner = A(n, f)
inner2 = A(inner, x)
body = A(f, inner2)
succ_l = L("n", L("f", L("x", body)))

# add = lambda m. lambda n. lambda f. lambda x. m f (n f x)
add_body = A(A(Var("m"), Var("f")), A(A(Var("n"), Var("f")), Var("x")))
add_l = L("m", L("n", L("f", L("x", add_body))))

# mul = lambda m. lambda n. lambda f. m (n f)
mul_body = A(Var("m"), A(Var("n"), Var("f")))
mul_l = L("m", L("n", L("f", mul_body)))

# Helpers to build terms

def succ_term(a):
    return A(succ_l, a)


def add_term(a, b):
    return A(A(add_l, a), b)


def mul_term(a, b):
    return A(A(mul_l, a), b)

Trace 1: Expanding `(n+1)(n+2)`#

We expand the multiplication of two successors. This shows how the lambda term unfolds, after which the algebraic proof uses induction.

# (n+1)(n+2) in lambda calculus
n = Var("n")
term = mul_term(succ_term(n), succ_term(succ_term(n)))

for i, s in enumerate(trace_reduce(term, max_steps=6)):
    print(f"{i}: {show(s)}")

(((lambda m. (lambda n. (lambda f. (m (n f))))) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n)) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n)))
((lambda n0. (lambda f. (((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n) (n0 f)))) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n)))
(lambda f. (((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n) (((lambda n. (lambda f. (lambda x. (f ((n f) x))))) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n)) f)))
(lambda f. ((lambda f. (lambda x. (f ((n f) x)))) (((lambda n. (lambda f. (lambda x. (f ((n f) x))))) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n)) f)))
(lambda f. (lambda x. ((((lambda n. (lambda f. (lambda x. (f ((n f) x))))) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n)) f) ((n (((lambda n. (lambda f. (lambda x. (f ((n f) x))))) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n)) f)) x))))
(lambda f. (lambda x. (((lambda f. (lambda x. (f ((((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n) f) x)))) f) ((n (((lambda n. (lambda f. (lambda x. (f ((n f) x))))) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n)) f)) x))))
(lambda f. (lambda x. ((lambda x. (f ((((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n) f) x))) ((n (((lambda n. (lambda f. (lambda x. (f ((n f) x))))) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n)) f)) x))))

Trace 2: Expanding `n^2` and `n` (mod 2 reasoning)#

We show the lambda expansion of n^2 = n * n. The congruence proof then uses the algebraic identity n^2 - n = n(n-1).

# n^2 in lambda calculus
n = Var("n")
term = mul_term(n, n)

for i, s in enumerate(trace_reduce(term, max_steps=6)):
    print(f"{i}: {show(s)}")

(((lambda m. (lambda n. (lambda f. (m (n f))))) n) n)
((lambda n0. (lambda f. (n (n0 f)))) n)
(lambda f. (n (n f)))

Trace 3: Expanding `(2n)^2`#

Here we expand 2n as add n n and then square it. The proof that the result is divisible by 4 uses arithmetic lemmas, but the expansion shows the computation structure.

n = Var("n")
term = mul_term(add_term(n, n), add_term(n, n))

for i, s in enumerate(trace_reduce(term, max_steps=6)):
    print(f"{i}: {show(s)}")

(((lambda m. (lambda n. (lambda f. (m (n f))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n)) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n))
((lambda n0. (lambda f. ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n) (n0 f)))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n))
(lambda f. ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n) ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n) f)))
(lambda f. (((lambda n0. (lambda f. (lambda x. ((n f) ((n0 f) x))))) n) ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n) f)))
(lambda f. ((lambda f. (lambda x. ((n f) ((n f) x)))) ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n) f)))
(lambda f. (lambda x. ((n ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n) f)) ((n ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n) f)) x))))
(lambda f. (lambda x. ((n (((lambda n0. (lambda f. (lambda x. ((n f) ((n0 f) x))))) n) f)) ((n ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n) f)) x))))

Trace 4: Expanding `(2n+1)^2`#

We expand (2n+1) as add (add n n) 1. The congruence argument then uses the algebraic identity (2n+1)^2 - 1 = 4n(n+1).

n = Var("n")
one_l = succ_term(zero_l)
term = mul_term(add_term(add_term(n, n), one_l), add_term(add_term(n, n), one_l))

for i, s in enumerate(trace_reduce(term, max_steps=6)):
    print(f"{i}: {show(s)}")

(((lambda m. (lambda n. (lambda f. (m (n f))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n)) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n)) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x)))))
((lambda n0. (lambda f. ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n)) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x)))) (n0 f)))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n)) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x)))))
(lambda f. ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n)) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x)))) ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n)) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x)))) f)))
(lambda f. (((lambda n0. (lambda f. (lambda x. (((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n) f) ((n0 f) x))))) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x)))) ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n)) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x)))) f)))
(lambda f. ((lambda f. (lambda x. (((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n) f) ((((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x))) f) x)))) ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n)) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x)))) f)))
(lambda f. (lambda x. (((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n) ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n)) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x)))) f)) ((((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x))) ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n)) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x)))) f)) x))))
(lambda f. (lambda x. ((((lambda n0. (lambda f. (lambda x. ((n f) ((n0 f) x))))) n) ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n)) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x)))) f)) ((((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x))) ((((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n)) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x)))) f)) x))))

Trace 5: Induction Step for Sum of Odds#

We document the recursive structure of the sum‑of‑odds identity:

sum_odds(n+1) = sum_odds(n) + (2n+1).

This is the lambda‑calculus shape that the induction proof follows.

# We show the lambda shape of the step, not full recursion.
# The proof uses the algebraic identity in the induction step.

n = Var("n")
sum_odds_n = App(Var("sum_odds"), n)
term_left = add_term(sum_odds_n, add_term(add_term(n, n), succ_term(zero_l)))
print("sum_odds(n+1) expands to:", show(term_left))

sum_odds(n+1) expands to: (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (sum_odds n)) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) n)) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (lambda f. (lambda x. x)))))

Remark

There are two layers in this chapter:

The witness objects are lambda-level programs defined for all n by Church iteration.
The verification cells are decidable checkers implemented via Python integer decoding, used as executable documentation.

A fully internal lambda-only checker (Church-defined equality and modulo) is possible but much slower in Python.

Exercise

Re-derive and re-check Theorem 1: show that \(2 \mid n(n+1)\) for all \(n\). Run the provided certificate and verify it for a small range.
Use Theorem 1 to derive \((2n+1)^2 - 1\) is divisible by \(8\), and implement the witness in terms of the existing building blocks. Verify it for a small range.
Implement sum_odds_ind (sum of first n odd numbers) as Church iteration and verify \(1+3+\cdots+(2n-1)=n^2\) for a small range. Write the induction step in words.
Pick one symbolic rewrite trace (for example, expanding \((2n+1)^2\)) and print the first few beta-reduction steps with trace_reduce. Explain what algebraic identity the reductions correspond to. See solutions: Exercise 9 (Induction Proofs as Lambda Certificates)

Summary#

Church numerals can drive induction-style computations by iterating a step function over a state.
A typical certificate is a witness-producing iterator paired with a decidable checker.
Congruence statements can be handled by building witnesses for divisibility and composing previously proved facts.
Symbolic beta-reduction traces explain why the induction step has the algebraic shape it does.
Next: Chapter 10 focuses on tooling and interactivity for experimenting with reductions and proof terms.

9. Induction Proofs as Lambda Functions (Church Style)

Contents

9. Induction Proofs as Lambda Functions (Church Style)#

Roadmap#

Setup (Church Numerals and Arithmetic)#

Induction Template in Lambda Form#

Visual: Unrolling the Induction Iterator#

Lambda Witness Proof Objects + Fast Decidable Checks#

Proof Script 1 (Lambda-Induction): \(2 \mid n(n+1)\)#

Proof Script 2 (Lambda-Induction): \(n^2 \equiv n \pmod{2}\)#

Proof Script 3 (Lambda-Induction): \((2n)^2 \equiv 0 \pmod{4}\)#

Proof Script 4 (General Induction Object): \((2n+1)^2 \equiv 1 \pmod{8}\)#

Proof Script 5 (Lambda-Induction): \(1+3+\cdots+(2n-1)=n^2\)#

Theorem 1 in Pure Lambda Terms (Detailed)#

Theorem 2 in Pure Lambda Terms (Detailed)#

Theorem 3 in Pure Lambda Terms (Detailed)#

Theorem 4 in Pure Lambda Terms (Detailed)#

Theorem 5 in Pure Lambda Terms (Detailed)#

Symbolic Rewrite Traces (Lambda Calculus)#

Trace 1: Expanding (n+1)(n+2)#

Trace 2: Expanding n^2 and n (mod 2 reasoning)#

Trace 3: Expanding (2n)^2#

Trace 4: Expanding (2n+1)^2#

Trace 5: Induction Step for Sum of Odds#

Summary#

Trace 1: Expanding `(n+1)(n+2)`#

Trace 2: Expanding `n^2` and `n` (mod 2 reasoning)#

Trace 3: Expanding `(2n)^2`#

Trace 4: Expanding `(2n+1)^2`#