Native PA language reference

This page states the object language accepted by Peano Lab. It is deliberately small: natural-number terms, first-order formulas, and no primitive division, remainder, exponentiation, lists, sets, primes, or quadratic residues. Every larger mathematical notion in the library expands to this grammar before the kernel sees it.

The interactive PA Proof Explorer uses this reference for every linked formal-proof line.

Terms

The kernel term grammar is

\[ t ::= x \mid 0 \mid S(t) \mid t+t \mid t*t. \]

Surface form	Meaning
x	a named free or bound variable at the surface
0	zero
S t	successor of t
t + u	addition
t * u	multiplication
1, 2, …	notation expanded to successor numerals

Bound variables are converted to de Bruijn indices internally. Names are a parser and pretty-printer convenience; alpha-renaming does not change the kernel term.

Multiplication binds more tightly than addition. Parentheses are always available and should be used liberally in generated statements.

Formulas

The kernel formula grammar is

\[ \varphi ::= t=u \mid \bot \mid \varphi\to\varphi \mid \varphi\land\varphi \mid \varphi\lor\varphi \mid \forall x.\varphi \mid \exists x.\varphi. \]

The ASCII surface spellings are:

t = u
false
A -> B
A /\ B
A \/ B
forall x. A
exists x. A

Negation is notation, not another formula constructor:

\[ \neg A \;:=\; A\to\bot, \]

written ~A. Chained quantifiers such as forall x y. A expand to nested single binders.

Conservative mathematical relations

Familiar arithmetic vocabulary is expressed relationally and expanded before checking. Examples include:

Informal notion	Native relational shape
\(a\le b\)	exists k. b = a + k
\(a<b\)	exists k. b = a + S k
\(a\mid b\)	exists k. b = a * k
\(a\equiv b\pmod m\)	balanced additive witnesses for a common multiple of m
quotient and remainder	n = d*q + r together with the expanded bound \(r<d\)
finite sequence entry	a Gödel-\(\beta\) relation
finite sum or product	a coded prefix trace with a functional endpoint
quadratic residue	existence of a square congruent to the value modulo the modulus

These are not new kernel symbols. The generated theorem pages show the exact fully expanded formula that is actually parsed and checked.

What the language intentionally lacks

There are no primitive terms for /, %, subtraction, powers, gcd, lists, finite products, primality, or Legendre symbols. There are also no predicate variables, so a single polymorphic object-language theorem quantifying over an arbitrary predicate is unavailable. Induction is instantiated for each concrete formula by the proof language.

This distinction matters when reading the quadratic-reciprocity theorem. Its surface page may explain residues, parity, quotient sums, and finite prefixes, but its exact statement contains only the grammar above.

Parser examples

forall n. n + 0 = n
forall a b. (exists k. b = a + k) -> (exists k. S b = a + k)
forall p a. ~(p = 0) ->
  (exists x u v. x * x + p * u = a + p * v) \/
  ~(exists x u v. x * x + p * u = a + p * v)

The final example illustrates an expanded decidability statement for a quadratic-residue relation. It adds no Boolean or classical oracle.

Source of truth

The executable definitions live in kernel/terms.py and kernel/formulas.py. The kernel chapter explains how formulas and certificates meet; axioms and rules lists the only arithmetic axiom constants and the proof constructors that can use them.