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.
-
-
-
-
-
is a term that can be subsituted for
in
without any of its variables becoming unquantified.
Inference Scheme
- from
and
, infer
- from
, infer
- from
, infer
can be any formula obtained by renaming variables in
.