PA1
∀ x. ¬S x = 0Terms
Terms are variables, 0, S t, t + u, and t * u. Numerals are surface expansions.
Formulas
Formulas use equality, bottom, implication, conjunction, disjunction, universal quantification, and existential quantification. Negation and ≤ are conservative surface expansions.
Read the full language reference.
Arithmetic axioms PA1–PA6
PA2
∀ x. ∀ y. S x = S y → x = yPA3
∀ x. x + 0 = xPA4
∀ x. ∀ y. x + S y = S (x + y)PA5
∀ x. x · 0 = 0PA6
∀ x. ∀ y. x · S y = x · y + xInduction
Induction is checked for each concrete first-order motive.
Cut
Cut shares a checked proof but is not an arithmetic axiom.
DNE
DNE belongs only to separately labelled classical mode and is not authority for this QR stack.
All native proof constructors
HypImpIntroImpElimCutAndIntroAndElimLAndElimROrIntroLOrIntroROrElimBotElimForallIntroForallElimExistsIntroExistsElimEqReflEqSymEqTransCongSCongAddCongMulEqSubstDNEAxiomInd