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]
          7. (induction scheme)

          Inference Scheme

          1. from and , infer
          2. from , infer
          3. from , infer

          can be any formula obtained by renaming variables in .

          Backlinks

          ZFC: Zermelo-Fraenkel Set Theory with Choice [000I]

            ZFC is a pure set theory meaning that every object is a set. It uses the same logical axiom scheme and inference scheme as PA - but the resulting axioms are different.

            The Zermelo-Fraenkel axioms are (TODO: write them out).

            1. Extensionality
            2. Pairing
            3. Union
            4. Power set
            5. Infinity
            6. Foundation
            7. Choice
            8. Separation scheme
            9. Replacement schme

            PA can reason about ZFC [001I]

              A proof in ZFC ist just a finite string of symbols. By encoding strings as natural numbers statements about proofs can be translated to statements about natural numbers and thus reasoned about within PA.