Consistent first-order theory

A theory is consistent when it does not derive a contradiction. By first-order completeness, this is equivalent to having a model.

A first-order theory is consistent when it has no formal proof of a contradiction. This syntactic property concerns the specified calculus; its equivalence with having a first-order model uses the completeness theorem.

A consistent set of first-order sentences is maximal when adding any new sentence makes it inconsistent. It is then deductively closed and decides every sentence by containing exactly one of it and its negation. Conversely a consistent deductively closed set that decides every sentence is maximal. Merely listing a finite axiom set for a complete theory does not make that raw list maximal: maximality applies to the deductive closure.

A first-order consistent theory is maximally consistent when it has no proper consistent extension in its fixed language. It decides each first-order sentence or its negation.

After fixing a Gödel numbering, the formal consistency statement $\mathrm{Con}(T)$ asserts that no natural number codes a $T$-proof of a contradiction. For a recursively axiomatized theory, this is an arithmetical sentence expressible inside any sufficiently strong base theory.

For adequate arithmetic provability predicates, the arithmetized deduction theorem identifies inconsistency of $S+\neg {\mathrm{Con}}_S$ with $S$-provability of ${\mathrm{Con}}_S$. Formalized second incompleteness gives ${\square }_S{\mathrm{Con}}_S\to {\square }_S\perp$. Contraposition yields the displayed conditional. This is an internal theorem and does not license removal of its consistency premise.

If $T$ is a consistent, recursively axiomatized theory containing enough arithmetic, then $T$ does not prove $\mathrm{Con}(T)$. The consistency assumption is external: an inconsistent theory proves every sentence, including its formal consistency statement.

Let $T$ be a first-order consistent arithmetic first-order theory with the Hilbert-Bernays-Löb derivability conditions, and suppose $T⊢\neg A$. Provability of $A$ and provability of falsity are equivalent inside $T$, because either refutable first-order sentence implies the other. Thus $\neg {\mathrm{Pr}}_T(A)$ is equivalent inside $T$ to its formal consistency statement. The second incompleteness theorem gives $T⊬\neg {\mathrm{Pr}}_T(A)$.

For theories $T,S$ extending a fixed base theory, one consistency-strength comparison iswhere $C_T$ is the set of consequences of $T$ and $\mathrm{Cons}$ is the chosen class of formal consistency statements. Its strict part $T{<}_{\mathrm{Cons}}S$ means $T{\le }_{\mathrm{Cons}}S$ but not $S{\le }_{\mathrm{Cons}}T$.

A relative-consistency result constructs a model of a first-order theory $S$, or interprets its proofs, from the assumed consistency of a background theory $T$. It establishes $\mathrm{Con}(T)\Rightarrow \mathrm{Con}(S)$ in the stated metatheory, not an unconditional proof of consistency. For independence of an axiom $\phi$ from $S$, obtain consistent models of both $S+\phi$ and $S+\neg \phi$, relative to the background assumption.

Let $T=\mathrm{ZFC}+\text{“there is a worldly cardinal”}$ and $T^{\ast }=\mathrm{ZFC}+\mathrm{Con}(\mathrm{ZFC})$. A worldly $\kappa$ makes $V_{\kappa }$ a model of ZFC, and arithmetic absoluteness for a rank-initial model makes it a model of $T^{\ast }$, so $T$ proves $\mathrm{Con}(T^{\ast })$. If $T^{\ast }$ proved $\mathrm{Con}(T)$, then the stronger theory $T$ would prove its own consistency, contradicting the Gödel second incompleteness theorem. Thus, assuming consistency, $T^{\ast }{<}_{\mathrm{Cons}}T$.

Starting from a recursively axiomatized theory $T_0$, defineAssuming consistency, Gödel second incompleteness theorem makes every step strict in the consistency-strength preorder, while the effective union $T_{\omega }={\bigcup }_{n<\omega }{T}_n$ lies strictly above every finite stage.

Consider extending $S+{\mathrm{Con}}_S$ by a rule sending every ${\mathrm{Con}}_A$ to ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$. Put $A=S+\neg {\mathrm{Con}}_S$. The initial consistency axiom proves ${\mathrm{Con}}_A$ by the negated-consistency extension theorem, so the rule proves ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$. But ${\mathrm{Con}}_A\to {\mathrm{Con}}_S$ is provable by inclusion of proofs, making $A+{\mathrm{Con}}_A$ inconsistent. Arithmetic verifies its finite contradiction proof. Thus the unrestricted rule proves both that theory's consistency and inconsistency. This differs from an externally justified progression along specified sound theories.

Every theory containing an inconsistent subtheory is inconsistent, because the same finite derivation of contradiction remains available.