First-order theory

A first-order theory is a set of sentences in one first-order language. Depending on convention, the term may instead mean its deductive closure.

This is a theory formulated in first-order logic.

An arithmetic theory is sound if all its theorems hold in the standard natural numbers. Arithmetic soundness implies consistency and rules out a proof of the negation of a true sentence. It is a semantic property, distinct from effective axiomatizability.

Robinson arithmetic is a weak finitely axiomatized first-order theory sufficient for numeralwise representation of computable finite calculations and the diagonal lemma. Its extensions are sufficiently strong for the soundness-based incompleteness argument.

A partial type over a first-order theory $T$ is a set of first-order formulas in a fixed finite tuple of variables which is jointly consistent with $T$. A tuple realizes it when it satisfies every formula in the set. A complete type additionally decides every formula in those variables.

The quantifier-free type of a tuple records all atomic and negated atomic formulas it satisfies, equivalently all quantifier-free formulas. Equal such types identify the generated substructures by sending each term value at one tuple to the value of the same term at the other tuple. Equality formulas make this correspondence well defined, and the relational formulas make it an isomorphism.

For $A\subseteq M$, an A-type over first-order structure $M$ is a set of formulas in a fixed finite tuple of variables, with parameters in $A$, consistent with the complete theory of $M$ expanded by constants for $A$. Every finite subset is realized in $M$. A complete type decides all formulas in its variables over those parameters.

A partial type is nonprincipal when it is not a principal partial type. Equivalently, for every formula $\theta (\mathbf{x})$ consistent with $T$, some $\psi \in p$ makes $\theta \wedge \neg \psi$ consistent with $T$. This is the exact extension property needed in the Henkin construction proving the omitting types theorem.

A first-order theory locally omits a family $\Gamma (\mathbf{x})$ if every formula $\theta (\mathbf{x})$ consistent with it has a consistent refinement $\theta \wedge \neg \gamma$ for some $\gamma \in \Gamma$. Equivalently no consistent formula implies all of $\Gamma$. In a countable language the omitting types theorem converts this local condition into a countable model with no realization of the family.

A partial type $p(\mathbf{x})$ is principal over $T$ if some formula $\theta (\mathbf{x})$ with $T\cup \{\exists \mathbf{x}\theta \}$ consistent implies each formula of $p$ modulo $T$. For complete types this is the usual notion of an isolated type. For an incomplete type, the isolating formula need not belong to the type itself.

A semidecidable axiomatization is a computably enumerable set of axioms. Its set of formal theorems is also computably enumerable by dovetailing over finite proofs.

The Craig trick converts an enumeration $A_1,A_2,\dots$ of axioms into a decidable equivalent set by replacing $A_i$ with a syntactically self-indexing repetition containing $i$ copies of $A_i$. A candidate of length $m$ can only encode one of the first $m$ axioms, so membership is decidable after computing that finite prefix.

The construction proves Craig's theorem: every computably enumerable axiomatizable theory has an equivalent decidable axiom set.

In a conservative language extension, attach a fresh nullary predicate $P_i$ to the $i$th axiom $A_i$ and use a self-indexing copy of $P_i\wedge A_i$. The fresh tag makes each new axiom independent of all the others, while forgetting the tags recovers exactly the original-language consequences. The Craig trick makes the resulting axiom set decidable.

A Gödel numbering assigns natural numbers effectively to symbols, formulas, and finite proofs. Syntactic predicates such as “$p$ codes a proof in $T$ of the formula with code $q$” can then be represented by arithmetical formulas.

For an effective Gödel numbering $M\mapsto \#M$, the quotation $d(M)=c_{\#M}$ is a Church numeral coding the syntax of $M$. It is not a code of a beta equivalence class. The operations taking syntax codes to the code of an application, or to the code of the numeral itself, are total computable functions and hence lambda-definable functions.

Let $A$ code application and $C$ code numeral quotation. For a lambda term $F$, choose a fresh $x$ and put $H=\lambda x.F(Ax(Cx))$ and $Q=Hd(H)$. Then $Ad(H)(Cd(H)){\equiv }_{\beta }d(Q)$, so $Q{\equiv }_{\beta }Fd(Q)$. This diagonal argument uses the syntax of the actual term $Q$, including any free variables, not an equivalence-class code.

A natural number coding a finite syntactic object under a fixed Gödel numbering. For program descriptions it records a function in intension; different codes may denote the same function in extension.

For an effectively axiomatized arithmetic theory, a arithmetical provability predicate expresses that a formal proof of the sentence with a specified code exists. If axioms are only enumerated, proof certificates also record finite stages at which their axioms appear. The resulting predicate is arithmetically expressible.

For a finite list $(a_0,\dots ,a_{r-1})$ of nonnegative integers, encode its length with the exponent of two and its entries with the following prime numbers: $2^r{\prod }_{j<r}{p}_{j+2}^{a_j+1}$, where $p_i$ is the $i$th prime number. Unique prime factorization recovers both the length and entries. Requiring positive exponents on exactly the prescribed consecutive primes also makes validity decidable. Nesting list descriptors therefore gives a Gödel encoding of deterministic finite automata and other finite syntactic objects.

Peano arithmetic is the first-order theory of the natural numbers with zero, successor, addition, multiplication, order, and the induction scheme.

This subsystem of second-order arithmetic allows comprehension for arithmetical formulas and induction in its standard restricted presentation. Its first-order arithmetical consequences are those of Peano arithmetic. It is a useful base for comparing well-quasi-ordering principles with ordinal notation systems without assuming their global well-foundedness.

Primitive recursive arithmetic formalizes primitive recursive functions, their defining equations, and quantifier-free induction. It is a weak arithmetic base for coding finite syntax and checking effective proof reductions. Assertions that a combinatorial principle implies formal consistency statement must specify such a base or another arithmetic metatheory.

Gentzen's consistency argument associates finite arithmetic derivations with effective ordinal notations below epsilon zero. An alleged contradiction admits an effective proof reduction preserving the contradictory end-sequent and strictly decreasing the assigned ordinal. Termination would therefore produce a normal contradiction, excluded by inspection of the logical rules and true atomic axioms. This explains why the relevant transfinite induction principle implies formal consistency statement. For a finite slow-well-ordering formulation one additionally needs the controlled-termination miniaturization theorem, rather than assuming that ordinary proof reductions have linearly growing size. The reduction program is discussed in math.stanford.edu/~feferman/papers/reductive.pdf .

An internally finite subset of $\{0,\dots ,c-1\}$ can be represented in Peano arithmetic by a product of distinct prime numbers: multiply the $e$th prime number exactly when $e$ belongs to the subset. Divisibility by that prime recovers membership. Arithmetic induction proves existence of this code even for a definable subset with a nonstandard cutoff in a nonstandard model of Peano arithmetic.

The theory of true arithmetic consists of all first-order arithmetic sentences true in the standard natural-number structure. It is complete but not computably enumerable.

Every nonempty definable set of natural numbers has a least element. Over the usual arithmetic language, this principle is equivalent to the induction scheme.

The well-ordering principle quantifies over all nonempty subsets of the natural numbers; in first-order arithmetic this entry is its definable-set schema.

A nonstandard model of Peano arithmetic is a model not isomorphic to the standard natural-number structure. It contains the standard numerals as an initial segment and also contains elements larger than every standard numeral.

In a model of Peano arithmetic, an element realizes this partial type exactly when it is not a standard numeral. A model omitting it is isomorphic to the standard natural-number structure. For a complete consistent extension $T$ of arithmetic, the type is nonprincipal exactly when $T$ is the theory of true arithmetic: apply the omitting types theorem in one direction and use an actual standard witness to refute any proposed isolating formula in the other. For incomplete theories, a principal partial type can still be omitted by some models.

The standard cut is the external initial segment consisting of the interpretations of the standard numerals. It is not definable, even with parameters, inside the nonstandard model.

If a definable property in a nonstandard model of Peano arithmetic holds of every standard natural number, then it holds of some nonstandard element. Equivalently, a definable set containing the entire standard cut of a nonstandard model of arithmetic must overspill beyond it.

This is the arithmetic case of overspill, which also applies to internal subsets of nonstandard extensions in analysis.

For every one-variable arithmetical formula $\theta (x)$, a sufficiently strong theory of arithmetic has a sentence $\gamma$ satisfying $\gamma \leftrightarrow \theta (┌\gamma ┐)$.

A fixed point of the negated arithmetic provability predicate for a computably enumerable arithmetic theory $T$. Consistency excludes a proof of $G$, because a genuine proof is arithmetically verifiable and contradicts the fixed-point assertion. Omega-consistency excludes a proof of its negation. For a consistent theory extending Robinson arithmetic, this sentence is true in the standard natural numbers.

This diagonal sentence says that any proof of itself has a no-later proof of its negation. A proof of $R$ contradicts finite verification that no earlier opposite proof exists. A proof of its negation, together with finite verification that no earlier proof of $R$ exists, proves the displayed universal condition and hence $R$. Thus consistency alone excludes both proofs, strengthening the original omega-consistency form of incompleteness.

The diagonal lemma can be carried out uniformly: from a one-variable formula code, compute a sentence code whose assertion is equivalent to the original formula applied to that sentence code. The effective substitution operation is what turns a semantic diagonal argument into a productive function.

Every consistent recursively axiomatized extension of elementary arithmetic is incomplete. If it were complete, its theorem set would be decidable; representing that decision procedure and diagonalizing against it yields a contradiction.

Tennenbaum's theorem says that no countable nonstandard model of Peano arithmetic can have both addition and multiplication computable under a presentation of its domain by the natural numbers.

Choose disjoint computably enumerable, recursively inseparable sets $A,B$. A nonstandard arithmetic model internally codes the elements enumerated into $A$ below a nonstandard stage by divisibility by standard primes. If the model's addition and multiplication were computable, division by each standard prime would decide the coded standard set. It would contain $A$ and avoid $B$, contradicting recursive inseparability.

A class of structures is first-order axiomatizable when it is exactly the class of models of some first-order theory. If extra constants are allowed, the corresponding class of reducts consists of structures that admit interpretations of those constants satisfying the theory.

The torsion-free groups are axiomatized by the group axioms together with, for every integer $n\ge 2$,

In the language with $\le$, total orders are axiomatized by reflexivity, antisymmetry, transitivity, and totality

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

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.

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.

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.

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

Every formal proof is a finite string and therefore uses only finitely many of the available assumptions.

A universal theory can be axiomatized by sentences whose quantifiers are all universal. Such sentences often forbid specified finite configurations.

The universal consequences $T_{\forall }$ of a first-order theory $T$ are all universal first-order sentences entailed by $T$. Their model class is exactly the class of substructures of models of $T$, up to structure embedding. This characterization follows from the diagram embedding criterion for universal theories.

A first-order theory has its class of first-order models closed under substructures of a first-order structure exactly when it is equivalent to its universal consequences $T_{\forall }$. If $A\models T_{\forall }$, then $T\cup \mathrm{Diag}(A)$ is consistent. Otherwise a finite logical conjunction $\delta$ of signed diagram of a structure sentences yields a universal consequence $\forall \mathbf{x}\neg \delta (\mathbf{x})$ false in $A$. The compactness theorem gives a first-order model of $T$ containing an embedded copy of $A$, and closure under substructures of a first-order structure implies $A\models T$. The converse is preservation of universal sentences. The diagram of a structure must include negated as well as positive atomic sentences so that the resulting map is an embedding, not just a homomorphism.

A universal sentence has the form $\forall \mathbf{x}\psi (\mathbf{x})$ with quantifier-free formula $\psi$, including an empty quantifier block. Its truth passes from a first-order structure to every substructure of a first-order structure: tuples from the smaller domain are also tuples of the larger domain, and quantifier-free truth agrees. Therefore a first-order theory of universal sentences has a first-order model class closed under substructures of a first-order structure.

A universal-existential sentence has a universal block followed by an existential block and a quantifier-free formula. Such axioms are preserved under unions of chains of structures: the universally chosen tuple occurs in one stage, whose existential witnesses remain in the union. An inductive first-order theory has an axiomatization by these sentences.

If failure of a property has a finite witness, one can often axiomatize the property by a universal sentence forbidding each possible finite witness. Compactness supplies finite witnesses when failure is expressed by inconsistency of an associated theory.