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.

A first-order model class is finitely axiomatizable in a fixed language if a finite set of sentences, equivalently one finite conjunction, has exactly that model class. Relative finite axiomatizability permits a fixed background theory and asks for only finitely many additional axioms. The distinction matters in an infinite scalar language, where even vector-space structure itself needs infinitely many named-symbol constraints.

A finite axiomatization of a class of structures is a finite set of first-order sentences whose first-order models are exactly that class. The existence of such a set is finite axiomatizability.

An arithmetic theory is bounded-complete if it proves every true closed formula with only bounded quantifiers. It then proves every true Sigma-1 sentence by choosing a standard witness. If it is also consistent, it cannot prove a false Pi-1 sentence: a standard bounded counterexample supplies a provable contradiction to that universal theorem. This arithmetic condition is distinct from bounded completeness of a statistical model or family.

No finite theory in the full language containing one function symbol for each scalar of an infinite field can axiomatize exactly its nonzero vector spaces. It mentions only finitely many symbols; changing an unused scalar function to violate preservation of zero leaves those finite sentences unchanged. Relative to the vector-space axiom schema, nonzeroness is instead the single axiom $\exists x(x\ne 0)$. Absolute finite axiomatizability and finite additional axiomatizability must be distinguished.

The existential theory of a structure is the set of existential sentences with quantifier-free matrices true in it. Its witnesses persist in extensions because quantifier-free truth is preserved by structure embeddings. It differs from an existential diagram, which additionally uses names for Elements.

A set of first-order sentences is satisfiable when it has a nonempty structure in which all its sentences are true. Truth of a sentence is independent of assignment in a first-order structure. The soundness theorem for first-order logic gives consistency from satisfiability, and Gödel's completeness theorem gives the converse for the standard classical deductive system.

In the language containing one binary equivalence relation $E$, require all classes to have size at most two and infinitely many classes of each of the two sizes. This is a complete theory: every countable model has countably many singleton classes and countably many doubleton classes, giving a class-by-class isomorphism; Downward Lowenheim-Skolem theorem then rules out a sentence separating arbitrary models. It is also an aleph-zero-categorical theory.

It is not finitely axiomatizable. Any finite fragment of the explicit infinitude schemes has a finite model with sufficiently many classes of each size; compactness theorem would make such a finite fragment suffice if any finite axiomatization existed. It is not model-complete: adjoining a new singleton preserves the theory, and subsequently giving that new point a partner also preserves the theory, while changing the existential partner formula at that point. Naming the singleton-class predicate removes this particular obstruction to elementary embeddings.

A first-order theory whose consequences can be decided by an algorithm that terminates on every input first-order sentence. Decidability of a chosen axiom set alone does not ensure decidability of its consequences.

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.

A first-order theory is omega-consistent when it never proves $\exists x\varphi (x)$ while proving $\neg \varphi (\bar{n})$ for every standard natural number $n$. Restricting the matrix to arithmetic bounded arithmetic formulas gives one-consistency. This condition concerns standard instances and is stronger than first-order consistency.

A bounded-complete complete omega-consistent arithmetic first-order theory is correct on every arithmetic first-order sentence. Completeness and first-order consistency make its theoremhood obey the Boolean truth tables. Omega-consistency ensures that every proved existential sentence has a provable standard numeral instance, since otherwise completeness refutes all such instances. Induction on logical formulas now identifies theoremhood with standard truth.

A first-order theory is Sigma-0 sound when every arithmetic bounded arithmetic sentence it proves is true in the standard natural numbers. For a first-order theory proving every true bounded arithmetic sentence, this is equivalent to first-order consistency: a false bounded theorem would have a provable bounded negation, and an inconsistent first-order theory proves the false bounded arithmetic sentence $0=1$.

Pi-1 soundness means that every closed Pi-1 theorem is true in the standard natural numbers. Consistency plus bounded completeness implies it, since a false universal bounded statement has a standard counterexample whose arithmetic verification is provable. It is weaker than full soundness and does not prevent a consistent arithmetic theory from proving a false Sigma-1 sentence.

A theory has Sigma-1 soundness if every Sigma-1 formula that is a closed theorem is true in the standard natural-number structure. It is weaker than full arithmetic soundness. Under bounded completeness it is equivalent to one-consistency. The standard interpretation matters: an existential statement can have a witness in a nonstandard model while having no standard witness.

An arithmetic theory is one-consistent if it does not prove $\exists x\delta (x)$ while proving every $\neg \delta (\overline{n})$, for a bounded arithmetic formula $\delta$ and all standard natural numbers $n$. If the theory proves all true bounded sentences, this is equivalent to Sigma-1 soundness: a false existential theorem has every standard instance refuted by bounded completeness; conversely a true witness and its provable negation contradict the assumption of a consistent first-order theory.

Given a bounded-complete one-consistent arithmetic first-order theory with a false theorem, enumerate first-order sentences and successively choose one-consistent one-sentence extensions. Every stage has Sigma-1 soundness, and a false Sigma-1 theorem in the union would already have a formal proof at one stage. The union is therefore one-consistent and complete while retaining the false theorem. It cannot be omega-consistent, since a complete bounded-complete omega-consistent first-order theory is sound.

Robinson arithmetic is a finitely axiomatized first-order theory in the language $0,S,+,\cdot$. Its seven axioms are the universal closures ofThey describe successor, addition and multiplication without an induction schema. Each calculation on particular standard numerals can still be verified: repeated use of the recursion equations proves, for example, $\overline{2}+\overline{3}=\overline{5}$. This finite computational strength is enough for representing computable finite calculations and for the diagonal lemma used in crude incompleteness theorem. Peano arithmetic adds induction for arbitrary arithmetic formulas.^[ref]

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.

A principal formula of a type is a logical formula first-order consistent with the base first-order theory that, modulo that first-order theory, implies every logical formula of the partial type. For a complete type it isolates a single point of the type space. A realized finite-tuple partial type in a finite first-order structure has such a logical formula by conjoining one distinguishing logical formula for each competing tuple with a different partial type.

Fix a tuple in a finite first-order structure. For every tuple of a different complete type, choose a logical formula true at the first tuple and false at the competitor. The finite conjunction selects only tuples of the desired partial type inside the first-order structure. Every implication from that conjunction to a member of the partial type is true in the first-order structure and hence belongs to its complete theory. Thus the conjunction isolates the partial type, even in an infinite first-order language.

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.

In the constant-free language with multiplication as its sole nonlogical symbol, every term in one free variable is $x^k$ for some $k\ge 1$. Every atomic formula $x^r=x^s$ holds at both zero and one. Hence every quantifier-free formula, being a finite Boolean combination of those atoms, has the same truth value at both points. They have the same quantifier-free type, and neither singleton is quantifier-free definable. Quantifiers distinguish them: $\forall y(xy=x)$ defines zero, while $\forall y(xy=y)$ defines one. These formulas do not rely on named zero or one constants.

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 replaces a computably enumerable axiom set by an axiom set that is a computable set with the same consequences. If the original set is nonempty, arrange a total computable sequence $A_1,A_2,\dots$ listing it with repetitions. This is possible even for a finite axiom set: once an axiom has appeared, output that axiom again at stages with no new output. An empty axiom set is already decidable.

Replace $A_i$ by the fully parenthesized conjunction $B_i$ of $i$ copies of $A_i$, using a fixed association convention. Each $B_i$ is logically equivalent to $A_i$. To test a candidate string of length $m$, compute only $A_1,\dots ,A_m$, construct the corresponding $B_i$, and compare strings. A conjunction of $i$ nonempty formulas has length at least $i$, so no later $B_i$ can equal the candidate. This finite computation decides membership.

The explicit total enumeration matters: waiting for the first $m$ distinct outputs of an arbitrary enumerator could run forever when it enumerates a finite set. The construction proves Craig's theorem.

Starting from a first-order consistent first-order theory, 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.

A logical formula weakly defines a total numerical function in a first-order theory when, at every standard input tuple, it proves the graph instance with the correct standard output and refutes graph instances with every incorrect standard output. This is numeralwise representation of the graph; it does not yet assert uniqueness against nonstandard outputs inside a first-order model.

Strong definability of a numerical function adds internal uniqueness of the output at every standard input tuple. Together with a proved correct instance, this says the first-order theory proves that the output logical formula is equivalent to logical equality with the correct numeral, for arbitrary potential outputs.

An arithmetical proof relation represents the effective relation that a natural number encodes a formal proof of the logical formula with a specified Gödel number. With the usual coding apparatus its proof-checking relation is bounded. Existential quantification over the formal proof code gives the ordinary arithmetical provability predicate.

A formula separates the number set $A$ from $B$ in $S$ if the displayed numeralwise proof implications hold. No decision is required outside $A\cup B$. In a consistent theory the sets must be disjoint. A diagonal sentence asserting the negation of its membership in a separator of provable from refutable codes is undecidable by the two direct contradiction cases.

A two-variable formula enumerates a set $A$ in a theory $S$ when membership supplies a standard numeral stage whose instance is provable, while nonmembership makes every standard-stage instance refutable. The notion contains these proof obligations, not merely a syntactic complexity restriction on the formula. With bounded completeness, a bounded formula whose existential closure defines a computably enumerable set provides such an enumerator.^[ref]

A Rosser provability predicate adds a bounded proof-order test to an arithmetical provability predicate: a proof of the sentence must occur before every proof of its negation. For a consistent theory it has the same standard extension as ordinary provability. Internally its behavior can differ: arithmetic proves $\neg R_T(┌\perp ┐)$ by splitting proof codes before and after a fixed proof of $\neg \perp$. This does not establish the usual consistency statement for ordinary provability.

The internal derivability conditions of a Rosser provability predicate depend on the proof numbering, even when the ordinary provability predicate is unchanged up to provable equivalence. Joining proofs of $A$ and $A\to B$ can increase their codes beyond the two bounds in the Rosser hypotheses, leaving the absence of earlier proofs of $\neg B$ unestablished. Internal modus ponens rule therefore needs a separate argument for the chosen numbering. Proof predicates can be constructed with different combinations of closure and introspection properties. ^[ref]. ^[ref].

If a first-order theory proves both $A$ and $\neg A$, the external truth of its Rosser provability predicate for $A$ depends on which side has the earlier formal proof code. A reserved least code for a formal proof of $\neg A$ makes the Rosser assertion false. Reserving the least code for a formal proof of $A$ makes it true. These are legitimate effective renumberings of the same formal proofs. Inconsistent first-order theories therefore require an explicit proof-order convention.

Assume the Hilbert-Bernays-Löb derivability conditions and the diagonal lemma. If $T+X$ proves ${\mathrm{Pr}}_T(┌Y┐)\to Y$ for every sentence $Y$, then $T⊢\neg X$. Take the single instance $Y=\neg X$ and discharge the assumption: $T⊢X\to (\square \neg X\to \neg X)$. This propositionally implies $T⊢\square \neg X\to \neg X$, and Löb's theorem gives $T⊢\neg X$. A diagonal proof is also possible using the Gödel sentence of the extension and formalized proof transfer, without appealing to Löb's theorem.

Assume the Hilbert-Bernays-Löb derivability conditions and the diagonal lemma. Choose $D$ with $T⊢D\leftrightarrow (\square D\to A)$. Necessitating the forward implication and using distribution and positive introspection gives $T⊢\square D\to \square A$. If $T⊢\square A\to A$, then $T⊢\square D\to A$, so the reverse fixed-point implication gives $T⊢D$. Necessitation gives $T⊢\square D$, and the preceding implications give $T⊢A$. No consistency assumption is needed for this implication between provability assertions.

For standard provability satisfying positive introspection, suppose $T⊢{\square }^{j}A\to A$ for some positive integer $j$. Positive introspection gives $T⊢\square A\to {\square }^{j}A$, hence $T⊢\square A\to A$. Löb's theorem yields $T⊢A$. The same argument applies with an already iterated first-order sentence in place of $A$.

In the Löb's theorem proof, $T⊢\square D\to \square A$ is obtained before any reflection assumption. Put $H=(\square A\to A)$. Propositional reasoning and the diagonal equation give $T⊢H\to D$. Necessitation and distribution yield $T⊢\square H\to \square D$, hence the displayed implication. This is the arithmetic interpretation of the Löb axiom in Gödel-Löb logic, and avoids necessitating a temporary assumption.

For an arithmetical provability predicate write $\square A={\mathrm{Pr}}_T(┌A┐)$. The conditions are: if $T⊢A$ then $T⊢\square A$; $T⊢\square (A\to B)\to (\square A\to \square B)$; and $T⊢\square A\to \square \square A$. The first is an external rule, while the latter two are internal theorems. They formalize proof verification, closure under modus ponens rule and positive introspection. None licenses reflection from a proved sentence $\square A$ to $A$.

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 obtained by adding the full first-order induction schema to Robinson arithmetic. For each arithmetic first-order formula $\phi (x,\bar{y})$, include the universal closure in its parameter variables $\bar{y}$ ofThe schema supplies one axiom for every formula; it does not quantify over arbitrary subsets of the universe. The order relation can be added by a defining axiom such as $x<y\leftrightarrow \exists z(y=x+Sz)$.

For example, induction on $x$ proves $0+x=x$, complementing the axiom $x+0=x$. Despite its intended interpretation in the natural numbers, Peano arithmetic also has non-standard models of arithmetic by the compactness theorem. First-order induction reaches every definable subset satisfying its hypotheses, without making the theory categorical.^[ref]

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.

Name every integer and add a new constant asserted to be prime and unequal to every named integer. Every finite part is satisfied by an ordinary prime outside a finite list, using Euclid's theorem. Compactness theorem with the elementary diagram gives an elementary extension with the desired prime. A countable elementary substructure retaining that prime cannot be isomorphic to the integer ring, since any unital ring isomorphism fixes every standard integer.

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 ┐)$.

For a computably enumerable first-order theory $T$ extending Robinson arithmetic, choose the standard arithmetic arithmetical provability predicate ${\mathrm{Prov}}_T$. The diagonal lemma, carried out in the weak base theory, gives a sentence $G$ withIf $T$ is consistent, $T$ cannot prove $G$: an actual finite proof would be verifiable in the weak base, so $T$ would prove both its provability and its unprovability. There is therefore no actual proof of $G$, and the displayed equivalence, true in the standard natural numbers, shows that this canonical $G$ is true there.

If $T$ is omega-consistent, it cannot prove $\neg G$ either. Such a proof would imply the existence of a proof code for $G$, while each standard numeral can be individually verified not to be such a code. Ordinary consistency suffices for unprovability of $G$; the original argument for unprovability of its negation uses the stronger hypothesis. Requiring the fixed-point equivalence in a sound weak base is important: an arbitrary equivalence provable only in an unsound extension need not yield a true sentence.

Assuming PA is consistent, the theory $S=\mathrm{PA}+\neg {\mathrm{Con}}_{\mathrm{PA}}$ is consistent by second incompleteness. Its false axiom $G=\neg {\mathrm{Con}}_{\mathrm{PA}}$ is provable, so the standard semantic biconditional $G\leftrightarrow \neg {\mathrm{Pr}}_S(┌G┐)$ is true with both sides false. Thus a true biconditional alone does not make an arbitrary sentence a true canonical Gödel sentence. A canonical Pi-1 construction adds the necessary syntactic or sound-base information. Truth, internal equivalence and canonical construction must be distinguished.

For a Gödel sentence $G\leftrightarrow \neg \square G$ with the Hilbert-Bernays-Löb derivability conditions, fix a refutable contradiction sentence $\perp$. Since $\perp \to G$ is provable, $\square \perp \to \square G$, giving $G\to \neg \square \perp$. For the reverse direction, $\square G$ implies both $\square \square G$ and $\square \neg \square G$, hence $\square \perp$. Contraposition gives $\neg \square \perp \to \neg \square G\to G$. This is an internal equivalence of sentences, not a rule asserting the theory's own consistency.

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.

For disjoint sets numeralwise enumerated by $P,R$, finite-initial-segment and total-comparison axioms let $H$ separate the first set from the second in the theory. For a member of the first set use a positive $P$ stage and finitely many refutations of $R$. For a member of the second set use its positive $R$ stage: earlier proposed $P$ stages are all refuted by a finite bounded proof, while later stages lose to that known $R$ witness. This proves a separator without inferring arbitrary negative facts from the mere Sigma-1 form of the enumerators.

For the standard Gödel sentence and Rosser sentence, the formalized Rosser unprovability theorem and $G\leftrightarrow \mathrm{Con}(T)$ yield $T⊢G\to R$. If $T+\mathrm{Con}(T)$ is consistent, the converse is unprovable under the usual formalized incompleteness hypotheses. A proof of $R\to G$ would give $\square \neg G\to \square \neg R$. Formalized negative unprovability identifies $\neg \square \neg R$ with $\mathrm{Con}(T)$ and $\neg \square \neg G$ with $\mathrm{Con}(T+\mathrm{Con}(T))$. The strengthened theory would then prove its own consistency, contradicting the Gödel second incompleteness theorem. The consistency assumption belongs to this strictness conclusion.

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.

Let $A,B$ be disjoint computably enumerable recursively inseparable sets, represented by existential arithmetic formulas with bounded computation witnesses $\alpha (x,y)$ and $\beta (x,z)$. In a non-standard model of arithmetic $M\models \mathsf{PA}$, the assertionholds at every standard bound $c$. The overspill lemma gives a nonstandard bound where it still holds. This no-clash condition matters: an arbitrarily chosen nonstandard computation stage need not preserve the external disjointness of the two enumerations.

Inside $M$, form the internally finite set $C=\{x<c:\exists y<c\alpha (x,y)\}$ and code it by the product of its corresponding prime numbers. Its standard trace contains $A$ and avoids $B$, since the finite standard witnesses for either enumeration lie below $c$. If the arithmetic operations of $M$ were computable, division by each standard prime would decide membership in this trace: search for $q$ and a standard remainder $r<p$ satisfying $a=pq+r$, where $a$ is the fixed code. The division algorithm in Peano arithmetic guarantees termination. This would give a computable set separating $A$ from $B$, a contradiction.^[ref]

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.

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 arithmetic first-order theory $T_0$ with the usual arithmetical provability predicates, defineIf every stage is first-order consistent, the Gödel second incompleteness theorem makes every step strict in the consistency-strength preorder: the next stage proves the preceding stage's formal consistency statement, which that preceding stage cannot prove. Every formal proof from the effective union $T_{\omega }={\bigcup }_{n<\omega }{T}_n$ uses only finitely many axioms and lies in one stage. Thus the union is first-order consistent under this hypothesis and lies strictly above every finite stage. Arithmetic soundness of $T_0$ is a sufficient starting assumption, since each added formal consistency statement is then true in the standard natural numbers.

Consistency of $T_0$ alone does not ensure consistency of the next stage. Assuming Peano arithmetic is first-order consistent, $T_0=\mathrm{PA}+\neg \mathrm{Con}(\mathrm{PA})$ is first-order consistent by the Gödel second incompleteness theorem. Proof inclusion makes it prove $\neg \mathrm{Con}(T_0)$, so adding $\mathrm{Con}(T_0)$ produces an inconsistent next stage. The hypotheses for a progression must therefore distinguish a consistent starting theory from consistency of all its iterates.

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.

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.

If a universal first-order theory in a first-order language with a constant entails an existential sentence with quantifier-free matrix, it entails a finite disjunction of closed-term instances of that matrix. Otherwise a first-order model of the first-order theory and all negated ground instances would have a ground-term substructure satisfying the first-order theory. An existential witness there is a tuple of closed-term values, contradicting its negated ground instance. Compactness theorem extracts finitely many instances.

Quantifier-free logical formulas have the same truth value in a substructure and its ambient first-order structure on tuples from the smaller carrier. First-order term evaluation agrees; atomic relations agree by restriction; Boolean connectives preserve agreement. A universally quantified quantifier-free matrix true on all ambient tuples is therefore true on all substructure tuples.

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 first-order model class axiomatized by a theory is closed under extensions exactly when it has an existential axiomatization. If $A$ satisfies all existential consequences of $T$, then $T$ is jointly satisfiable with the universal theory of $A$: any finite obstruction would negate a universal conjunction and produce a violated existential consequence. Embed a model of $T$ into a model elementarily equivalent to $A$, apply extension closure, and transfer truth back to $A$.

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.

A finite forbidden relational pattern can be excluded by a universal sentence. If a finite structure $F$ has distinct vertices $1,\dots ,m$, let ${\delta }_F(x_1,\dots ,x_m)$ say that the variables are distinct and have the required relations. Thenforbids that pattern. Taking one sentence for each forbidden finite pattern gives a universal first-order theory.

For a triangle-free graph, the forbidden diagram asserts that three distinct vertices are pairwise adjacent. To forbid an induced pattern, the diagram must specify absent relations as well as present ones. Forbidding an ordinary path on three vertices allows extra edges between its vertices; forbidding an induced path on three vertices does not. Thus the meaning of pattern determines the exact diagram. The construction explains why many local graph constraints are preserved under taking substructures.