In deductive logic, a consistent theory is one that does not produce a logical contradiction. A theory is consistent if it does not prove both a statement and its opposite. For example, if a theory proves "It is raining" and also proves "It is not raining," the theory is inconsistent. A theory is built from a set of starting statements called axioms. If a set of axioms can prove both a statement and its opposite, the set is inconsistent. A theory that proves all possible statements is inconsistent because it includes contradictions. In some logical systems, like classical logic, any inconsistent theory automatically proves all statements, making it trivial. Consistency is a rule-based idea, while its related concept, satisfiability, is about whether a theory can be true in some situation. A theory is satisfiable if there is a way to interpret its statements so that all axioms are true. This idea of satisfiability is similar to what "consistent" meant in older logic systems, though modern logic uses "satisfiable" instead.

In a sound logical system, any theory that can be true in some situation is consistent, but not all consistent theories can be true in a situation. If a logical system has rules that make the idea of consistency and satisfiability the same, the system is called complete. The completeness of propositional logic was proven by Paul Bernays in 1918 and Emil Post in 1921. The completeness of predicate logic was proven by Kurt Gödel in 1930. Consistency for certain types of arithmetic was proven by Ackermann, von Neumann, and Herbrand. Stronger logics, like second-order logic, are not complete.

A consistency proof is a way to show that a theory does not lead to contradictions. Early work in mathematical proof theory aimed to prove the consistency of all mathematics using finite methods, as part of Hilbert's program. However, Hilbert's program was challenged by the incompleteness theorems, which showed that strong proof systems cannot prove their own consistency if they are consistent.

Consistency can be proven using models, but it is often shown through rules alone, without needing to reference specific models. A process called "cut-elimination" in logic shows that if a system does not allow certain types of proofs, it avoids contradictions. This means the system is consistent because it cannot prove false statements.

Consistency and completeness in arithmetic and set theory

In arithmetic theories, such as Peano arithmetic, there is a complex connection between the consistency of the theory and its completeness. A theory is complete if, for every statement φ in its language, either φ or its opposite (¬φ) can be proven using the rules of the theory.

Presburger arithmetic is a system of rules for working with natural numbers and addition. This system is both consistent (it does not contain contradictions) and complete (it can prove or disprove every statement in its language).

Gödel's incompleteness theorems show that any strong enough theory of arithmetic that can be listed systematically (recursively enumerable) cannot be both complete and consistent. These theorems apply to theories like Peano arithmetic (PA) and primitive recursive arithmetic (PRA), but not to Presburger arithmetic.

Additionally, Gödel's second incompleteness theorem explains that the consistency of a strong enough, recursively enumerable theory of arithmetic can be checked by examining a specific statement, called the Gödel sentence. This sentence is a formal version of the claim that the theory is consistent. Therefore, the consistency of such a theory cannot be proven within the theory itself. This result also applies to other systems, such as Zermelo–Fraenkel set theory (ZF), which cannot prove their own Gödel sentence if they are consistent, as is generally believed.

Because the consistency of ZF cannot be proven within ZF itself, the idea of relative consistency becomes important in set theory and similar systems. If a theory T is consistent, and adding a new rule A to T (making it T + A) also keeps the system consistent, then A is said to be consistent with T. If both A and its opposite (¬A) are consistent with T, then A is independent of T.

First-order logic

In the context of mathematical logic, the turnstile symbol ⊢ means "provable from." For example, a ⊢ b means that b can be proven from a within a specific formal system.

Let S be a set of symbols. Let Φ be a maximally consistent set of S-formulas that includes witnesses.

An equivalence relation ∼ is defined on the set of S-terms. Two terms t₀ and t₁ are considered equivalent (t₀ ∼ t₁) if the statement t₀ ≡ t₁ is in Φ, where ≡ represents equality. The equivalence class of a term t, denoted as t̄, includes all terms that are equivalent to t. The set TΦ is defined as the collection of all such equivalence classes, written as TΦ := {t̄ | t ∈ Tₛ}, where Tₛ is the set of terms formed using the symbols in S.

The S-structure TΦ, also called the term-structure corresponding to Φ, is defined over TΦ. A variable assignment βΦ is established by assigning each variable x to its equivalence class x̄. The term interpretation associated with Φ is IΦ := (TΦ, βΦ).

For each S-formula φ, several points must be verified. First, it must be confirmed that ∼ is indeed an equivalence relation. Next, it must be shown that definitions (1), (2), and (3) are well-defined. This follows from the properties of ∼ and requires proving that (1) and (2) do not depend on the specific representatives chosen for equivalence classes. Finally, it must be verified that IΦ satisfies φ, which can be done using induction on formulas.

Model theory

In ZFC set theory with classical first-order logic, an inconsistent theory T is one where there is a closed sentence φ such that T includes both φ and its negation φ'. A consistent theory is one where certain logically equivalent conditions are true.