PA: Peano Arithmetic [0000]

Peano arithmetic is a formal axiomatic system. Infinitely many axioms can be built by replacing with formulas in the language of PA. In PA a theorem is a formula that is either an axiom or can be derived from finitely many axioms with finitely many rules of inference.

1. Logical Axiom Schemes [000J]

is a term that can be subsituted for in without any of its variables becoming unquantified.

2. Equality Axioms [000K]

3. Non-logical Axioms [000L]

(induction scheme)

Inference Scheme

from and , infer
from , infer
from , infer

can be any formula obtained by renaming variables in .