Peano arithmetic
This chapter develops a small first-order arithmetic theory. We add
equality, successor, quantifiers, substitution, and induction to classical
propositional logic, then prove an addition law and a concrete sum. Unlike
the sequent system of the previous chapter, this theory uses Hilbert style:
formulas are themselves assertions, and wff is the provable sort.
The propositional skeleton
This is the same Łukasiewicz system as the Hilbert calculus chapter.
Hilbert-style proofs repeatedly use a few short derived rules. We prove them once so later proofs can cite them.
a1i weakens a theorem with an antecedent, and syl composes two
implications.
Numbers
peano1 says zero is not a successor, and peano2 says that successor is
injective. Its converse, peano2r, would ordinarily follow from a congruence
principle; this small theory assumes it directly. The axioms use object-level
implication rather than rule hypotheses, so their use generally requires an
ax_mp step:
The equational layer
The theory needs to say how equivalent formulas and equal terms may replace one another, in the format of the Equality and normalization chapter:
A natural question: why introduce nat_eq when the theory already has =?
A @relation bundle needs its members in rule form, and the equality axioms
above are object-level implications — eq_trans is a formula about →, not
a rule the normalizer can chain. Rather than derive rule-form counterparts,
the theory keeps a separate judgment for the rewriting machinery; eq_congr
connects it back to = formulas.
Quantifiers
For quantifiers, we have generalization, distribution of ∀ over
implication, and vacuous quantification (note that ax_5’s p does not
depend on x). Generalization is written in rule form: it takes a proof of
p and produces a proof of ∀ x p. Here we apply it to an equality proved
without hypotheses:
Substitution and instantiation
As in the last chapter, substitution is an ordinary term with @rewrite
equations that push it through the syntax. Here it comes in two layers:
sb_f substitutes in a formula and normalizes along ↔, while sb_t
substitutes in a number term and normalizes along nat_eq:
ax_inst is instantiation. Its raw conclusion sb_f x t p is not intended to
be user-facing syntax. Instead, the @view and @recover annotations (from
Views and recovery) let a proof state the normalized
instance, and let the compiler recover t and p from that shape:
The rewrite rules push sb_f through =, then sb_t through suc and down
to the variable, and the emitted proof carries the conversion.
Addition and induction
Addition is defined by recursion on the right argument. peano5 is induction,
stated with sb_f explicit in both hypotheses. The @view on the induction
axiom uses two phantom binders, base and step, that absorb whatever the
hypotheses normalize to: the user supplies the base case and inductive step in
their already-substituted forms, and the rewrite rules reconcile them with the
sb_f shapes.
The left identity law is a common first induction. Lines l1–l7 build the
base case and the generalized step, and l8 closes:
The next theorem has no {x: nat} binder; its proof obtains x from the
sort’s @vars pool:
Two plus two
To close, here’s a concrete computation: unfold with add_suc twice and
add_0 once, lifting through suc with peano2r at each stage:
Even this small sum needs several congruence and transitivity steps. To
automate such proofs, register the recursion equations with @compute and
use conversion?. The lambda calculus chapter
demonstrates this approach.