Consistency proof

A metamathematical argument that a formal system cannot derive a contradiction. Gödel’s second incompleteness theorem shows that sufficiently strong, consistent systems cannot prove their own consistency by their own methods.

Formal system: A set of formal axioms and inference rules for deriving statements. Consistency is a property of a formal system’s derivations.
First-order logic: A formal logic with variables, quantifiers, predicates, and rules for inference. Many consistency results are stated for theories formulated in this logic.
Gentzen's consistency proof of Peano arithmetic: Gerhard Gentzen’s proof of Peano arithmetic’s consistency using transfinite induction up to ε₀. It exemplifies a consistency proof whose methods exceed those formalizable in Peano arithmetic.
Syntactic consistency: The absence of a formal derivation of contradiction in a deductive system. This is the proof-theoretic property that consistency proofs directly establish.
Contradiction: A statement asserting both a proposition and its negation, or a formal derivation of incompatible claims. A system is inconsistent when its rules let it derive a contradiction.
Soundness: A property of a proof system in which every derivable statement is semantically valid. Soundness can establish consistency when the system’s semantics are themselves consistent.
Hilbert's consistency proof for geometry: A relative consistency argument deriving the consistency of Euclidean geometry from that of real arithmetic. It shows how interpreting one theory inside another transfers a consistency question.
Semantic consistency: The existence of an interpretation in which a theory’s axioms are all true. A satisfying model gives a semantic counterpart to syntactic consistency.
Gödel numbering: A method that encodes symbols, formulas, and proofs as natural numbers. Gödel used numerical codes to make a system’s proofs part of arithmetic.
Completeness theorem: Gödel’s theorem that every first-order sentence true in all models is formally derivable. It connects syntactic consistency of first-order theories with having a model.

Linked from 10 pages