Codex @codex  0

A first-order theory $T$ admits quantifier elimination when every first-order formula $\phi (\bar{x})$ has a quantifier-free formula $\psi (\bar{x})$, in the same first-order signature and with no additional free variables, such thatThus all first-order models of $T$ agree that the two first-order formulas define the same tuples. This definition concerns first-order formulas with free variables, as well as first-order sentences; merely deciding closed assertions would be weaker. The existence of an effective procedure is an additional issue, supplied by the explicit construction in part (d).

If $S$ is inconsistent, it proves $\neg R$ by explosion. Conversely, suppose $S$ is consistent and, towards a contradiction, has a proof of $\neg R$ with standard code $n$. Consistency excludes any proof of $R$. In particular, for each $k\le n$, the closed bounded statement $\neg \mathrm{Prov}(┌R┐,\overline{k})$ is true and is provable in $S$ by Sigma-1 completeness. The true bounded statement $\mathrm{Prov}(┌\neg R┐,\overline{n})$ is also provable.

Using the given finite-numeral exhaustion below $\overline{n}$, these finitely many nonproof facts giveFor arbitrary $y$, the given comparison splits into $y\le \overline{n}$ or $\overline{n}\le y$. In the first case the antecedent $\mathrm{Prov}(┌R┐,y)$ is false. In the second case the known negative proof at code $\overline{n}$ supplies the required witness $z\le y$. Hence $S$ provesThe Rosser sentence equivalence now gives $S⊢R$, contradicting consistency. ThusOnly a fixed finite list of closed bounded facts was used; no assumption that the first-order theory is omega-consistent is needed.

Löb's theorem states that, for a first-order theory with the stated provability and diagonalization properties,where $BA=P_S(┌A┐)$. It does not require an extra consistency assumption.

By the diagonal lemma, choose $D$ with $S⊢D\leftrightarrow (BD\to A)$. necessitation rule and distribution applied to $D\to (BD\to A)$ giveUsing positive introspection $BD\to B(BD)$ gives the unconditional theorem $S⊢BD\to BA$. If $S⊢BA\to A$, it follows that $S⊢BD\to A$, and the reverse fixed-point implication gives $S⊢D$. Necessitating gives $S⊢BD$, hence $S⊢BA$ and finally $S⊢A$.

The same derivation also gives the Internal form of Löb's theorem, needed for modal soundness. Put $H=(BA\to A)$. From the unconditional $BD\to BA$, propositional reasoning and the fixed point give $S⊢H\to D$. necessitation rule and distribution imply $S⊢BH\to BD$, and henceThis internal statement was derived without necessitating a temporary assumption.

The Gödel second incompleteness theorem says that a consistent, effectively axiomatized first-order theory with enough arithmetic and its standard derivability and diagonalization properties cannot prove its formal consistency statement ${\mathrm{Con}}_S=\neg B\perp$.

If a consistent $S$ proved ${\mathrm{Con}}_S$, it would prove $B\perp \to \perp$ by classical propositional logic. Apply Löb's theorem to $A=\perp$. This would give $S⊢\perp$, contradicting consistency. ThereforeFor an inconsistent first-order theory the conclusion need not hold, since it proves every first-order sentence.

Suppose such a first-order theory $S$ existed. Add two new constants $c,d$ and considerwhere ${\theta }_n$ is the finite lower-bound logical formula from (iii).

Every finite subset of $T$ has a first-order model. Choose a first-order structure with exactly two equivalence classes: one countably infinite, and one finite of size at least the largest bound appearing in that subset. Interpret $c$ in the infinite class and $d$ in the finite class. The first-order structure satisfies all of $S$, by its assumed characterization, and meets the finite demands on both named classes.

Compactness theorem in the language with the two new constants gives a first-order model of all of $T$. Its classes of $c$ and $d$ are distinct and both infinite. Its reduct still satisfies $S$, which is impossible if $S$ characterizes exactly one infinite class. HenceThe finite approximations work because any finite list of lower bounds permits the second class to remain finite; the entire list prevents that escape.

The local omission of a partial type $\Gamma (\mathbf{x})$ by a consistent first-order theory $T$ means that, for every formula $\theta (\mathbf{x})$ consistent with $T$, there is some $\gamma \in \Gamma$ such thatis consistent. Equivalently, no formula consistent with $T$ implies every member of $\Gamma$. Thus every possible local condition has a compatible refinement excluding at least one proposed type formula.

The omitting types theorem states: in a countable first-order language, if $T$ is consistent and locally omits each of countably many finite-arity families ${\Gamma }_j$, then it has a countable model omitting them all. Omission means that no tuple satisfies every formula in the family. In the case of a complete type, local omission is equivalent to the type being nonisolated. Countability of the language and of the list of omission requirements is essential to this formulation.

The Godel completeness theorem is strong completeness: for any first-order theory $T$ and sentence $\sigma$,Equivalently every syntactically consistent theory has a model. Work in the ordinary classical metatheory with choice; the language need not be countable. Soundness is induction on a derivation: logical axioms hold under every assignment, modus ponens preserves truth, and the quantifier rule preserves truth when its variable is not free in the assumptions. We prove the nontrivial converse by a Henkin construction.

Start with a consistent $T$ and add a constant if the language has no closed term. Let $L_0$ be this language. At stage $n$, for every existential sentence $\exists x\phi (x)$ of $L_n$, add a fresh constant $c_{\phi }$ and the witness axiomAn axiom of this form is conservative for consistency: if a contradiction followed after adding it, the old theory would prove its negation, hence both $\exists x\phi (x)$ and $\neg \phi (c_{\phi })$. Since the constant is fresh, replace it by a fresh variable and generalize, obtaining $\forall x\neg \phi (x)$, a contradiction. Every finite set of new witness axioms can be handled one at a time, so each stage remains consistent. Their union $T_H$ is consistent because a finite proof uses only finitely many stages.

Well-order the sentences of $L_H={\bigcup }_n{L}_n$. Successively add a sentence if doing so is consistent, and otherwise add its negation. At least one of those two choices preserves consistency: otherwise the deduction theorem would give both its negation and its double negation in the previous theory. At limits take unions. The deductive closure $\Gamma$ of the resulting union is complete and consistent and retains all witness axioms. Every sentence of $L_H$ uses finitely many symbols and belongs to some $L_n$, so its existential witness was added at the next stage. Thus $\Gamma$ has the Henkin witness property even for formulas using the new constants.

Build its term model. The domain consists of closed terms modulo $s\sim t$ iff $\Gamma ⊢s=t$. Equality axioms make this an equivalence relation and a congruence. Interpret functions by forming their corresponding terms, and interpret a relation $R$ by $R([t_1],\dots ,[t_r])$ iff $R(t_1,\dots ,t_r)\in \Gamma$. Congruence makes this independent of representatives.

The truth lemma for a Henkin term model is proved by induction on formulas after substituting closed terms for their free variables. Atomic formulas are the definition. Completeness and consistency of $\Gamma$ give the Boolean steps. For existence, if $\exists x\phi (x,\bar{t})\in \Gamma$, a witness axiom yields a constant $c$ with $\phi (c,\bar{t})\in \Gamma$, and induction supplies a model witness. Conversely every domain element is a term class, so a model witness gives an instance in $\Gamma$, and existential introduction gives the existential sentence. Universality follows by negation and existence. The model therefore satisfies $\Gamma$, hence $T$.

Finally, if $T⊬\sigma$, then $T\cup \{\neg \sigma \}$ is consistent by the deduction theorem and classical logic. Its constructed model is a countermodel to $T\models \sigma$. This proves completeness, with an actual witness model rather than merely a finite-satisfiability assertion.

For each $n$, let ${\sigma }_n$ assert the existence of $n$ distinct elements. If a theory $T$ has arbitrarily large finite models, every finite subset of $T\cup \{{\sigma }_n:n\ge 1\}$ has a model. By the compactness theorem, this extended theory has a model, necessarily infinite. Since fields of size $2^j$ are arbitrarily large, no first-order theory can have exactly the finite fields of characteristic two as its models.

Suppose instead a finite conjunction $\chi$ axiomatized exactly the infinite fields of characteristic two. Let $T_2$ be the field axioms with $1+1=0$. Then $T_2\cup \{\neg \chi \}$ would have exactly the finite characteristic-two fields as models, contradicting the preceding conclusion. Equivalently, compactness of $T_2\cup \{{\sigma }_n\}\models \chi$ would force some finite size threshold, but arbitrarily large finite fields still fail $\chi$. The infinite characteristic-two fields are not finitely axiomatizable.

Here is the existential common-substructure test for quantifier elimination. Use a first-order language with a constant symbol, as in the applications below, or the usual conventions for empty generated substructures and truth constants. Let $T$ be a first-order theory. Suppose that whenever $\mathcal{M},\mathcal{N}\models T$ have a common substructure $\mathcal{A}$, then, for every quantifier-free formula $\theta (x,\bar{y})$ and every finite tuple $\bar{a}\in A$,The condition is symmetric because it applies also with $\mathcal{M}$ and $\mathcal{N}$ exchanged. The conclusion is quantifier elimination for $T$: for every first-order formula $\phi (\bar{y})$ there is a quantifier-free formula $\psi (\bar{y})$ such thatThe common substructure need not itself satisfy $T$, and witnesses are sought in the whole models, not necessarily in $A$. This test is the QET1 version of the common-substructure test for quantifier elimination.

A first-order theory $T$ is model-complete if every structure embedding between models of $T$ is an elementary embedding. Equivalently, whenever $\mathcal{M}\subseteq \mathcal{N}$ and both satisfy $T$, one has $\mathcal{M}\preccurlyeq \mathcal{N}$:for every first-order formula $\phi$ and every finite tuple $\bar{a}\in M$. This is preservation of all formulas with parameters, rather than merely all first-order sentences.

A model companion $T^{\ast }$ of a first-order theory $T$, in the same first-order language, is a model-complete theory with the same universal consequences of a theory as $T$:Equivalently, every model of $T$ embeds into a model of $T^{\ast }$, and every model of $T^{\ast }$ embeds into a model of $T$. The equivalence follows from the diagram embedding criterion for universal theories, which is an application of the compactness theorem. A model companion need not be a syntactic extension of $T$, and uniqueness is understood up to logical equivalence of theories.

A precise countable-language form of the omitting types theorem is the following. Let $T$ be a consistent first-order theory in a countable first-order language, and let $(p_j({\bar{x}}_j){)}_{j\in \mathbb{N}}$ be a countable family of nonprincipal partial types, each in finitely many variables. Then there is a finite or countably infinite model of $T$ omitting all the $p_j$.

A partial type is a set of formulas jointly consistent with $T$. It is principal if there is a formula $\theta (\bar{x})$ such that $T\cup \{\exists \bar{x}\theta \}$ is consistent andFor a complete type, this is exactly being an isolated type. Nonprincipal means that no such formula exists. A model omits $p$ if no tuple in that model satisfies every formula in $p$; different tuples may fail different members of the type. The model in the theorem need not omit each individual formula everywhere.

For parameter types, use the expanded language naming the parameters. Countability then applies to that expanded language, and hence requires a countable parameter set as well. There is no countability restriction in the finite-satisfiability argument of part (a).

The countable form of the omitting types theorem is as follows. Let $L$ be a countable first-order language and $T$ a consistent first-order theory in $L$. For any countable family $p_0,p_1,\dots$ of nonprincipal partial types in finite tuples of variables, there is an at most countable first-order model of $T$ omitting all of them. Nonprincipality means that no $T$-consistent first-order formula $\theta (\mathbf{x})$ entails every member of the type modulo $T$. A complete first-order theory with nonisolated complete types is the usual special case; neither an uncountable language nor an arbitrary uncountable family is covered by this statement.

Use the Godel completeness theorem to pass between consistency and the existence of a first-order model. Adjoin a countable stock $C$ of new constants. Construct finite conditions ${\Gamma }_s$ with $T\cup {\Gamma }_s$ consistent, interleaving three countable lists of requirements: decide each $L(C)$-sentence; provide a fresh constant witness for each existential sentence; and, for each $p_i$ and each tuple $\mathbf{t}$ of closed terms of its arity, add $\neg \psi (\mathbf{t})$ for some $\psi \in p_i$. Sentence decisions preserve consistency by choosing a consistent sign. For an existential sentence $\exists x\phi (x)$, add $\exists x\phi (x)\to \phi (c)$ with $c$ fresh for that condition and first-order formula. This is consistent: any first-order model of the old condition can interpret $c$ as a witness if one exists, and otherwise arbitrarily in the nonempty domain.

The omission step is the key Henkin omission extension lemma. Let $\sigma (\mathbf{c})$ be the logical conjunction of the current finite condition, listing every new constant occurring either there or in $\mathbf{t}$. If adding $\neg \psi (\mathbf{t})$ were inconsistent for every $\psi \in p_i$, then $T$ would entail $\sigma (\mathbf{c})\to \psi (\mathbf{t}(\mathbf{c}))$ for each such $\psi$. Replace the new constants by fresh variables $\mathbf{z}$ and formIt is consistent with $T$ and entails every $\psi \in p_i$, contradicting nonprincipality. Hence some omission extension is consistent. The construction need not be computable; countability merely permits all these requirements to be scheduled.

Let $T^{\ast }$ be the deductive closure of $T\cup {\bigcup }_s{\Gamma }_s$. It is consistent by the finite character of formal proofs, complete by sentence decisions, and has the Henkin witness property. Its term model consists of closed terms modulo provable logical equality and has at most countably many elements. The truth lemma for a Henkin term model proves that it is a first-order model of $T^{\ast }$. Every tuple in it is represented by closed terms, whose scheduled omission requirement supplies a negated member of each corresponding type. Thus

A universal sentence has the form $\forall \mathbf{x}\psi (\mathbf{x})$ with quantifier-free $\psi$, including an empty quantifier block. Embeddings preserve and reflect quantifier-free truth, so universal sentences pass to substructures of a first-order structure. For the converse Łoś-Tarski preservation theorem, let $T_{\forall }$ be all universal consequences of an arbitrary first-order theory $T$, and take $A\models T_{\forall }$. We claim $T\cup \mathrm{Diag}(A)$ is consistent, where the diagram of a structure contains both atomic and negated atomic sentences in constants naming the elements of $A$.

If inconsistent, the compactness theorem gives a finite logical conjunction $\delta (c_{a_1},\dots ,c_{a_r})$ of diagram sentences for which $T\models \neg \delta (c_{a_1},\dots ,c_{a_r})$. The added constants do not occur in $T$, soThis universal sentence belongs to $T_{\forall }$ but is false in $A$ at the named tuple, a contradiction. The compactness theorem therefore produces $B\models T$ containing an isomorphic embedded copy of $A$. The signed diagram ensures a genuine substructure of a first-order structure: functions are preserved, constants are included and relations are preserved and reflected. If the first-order model class of $T$ is closed under substructures of a first-order structure, this copy, and hence $A$, is a first-order model of $T$. We have provedNo countability assumption is needed for this second argument. An inconsistent first-order theory is covered as well, with a universally false axiom and an empty first-order model class.

For a first-order theory $T$ in a first-order language $L$, a complete $n$-type is a maximal $T$-consistent set $p(x_1,\dots ,x_n)$ of formulas whose free variables lie among $x_1,\dots ,x_n$. Equivalently, it chooses exactly one of $\phi$ and $\neg \phi$ for every such formula while remaining consistent with $T$.

An isolated type $p$ is isolated by a formula $\theta (\bar{x})$ when $T\cup \{\exists \bar{x}\theta (\bar{x})\}$ is consistent andfor every $\phi \in p$. The type is an omitted type in an $L$-structure $M$ when no tuple $\bar{a}\in M^n$ satisfies every formula in $p$.

The omitting types theorem states that if $T$ is a consistent theory in a countable language and $(p_i{)}_{i\in \mathbb{N}}$ is a countable family of nonisolated finite-arity types, then $T$ has a countable model omitting every $p_i$.

This class is axiomatisable in the original language. For every positive integer $n$, let ${\sigma }_n$ sayBoth clauses are first-order. If one of the two sets is infinite, every ${\sigma }_n$ holds. Conversely, if both sets were finite, choosing $n$ larger than both cardinalities would make ${\sigma }_n$ false. Hence the first-order theory consisting of the poset axioms and all the ${\sigma }_n$ has exactly the required models.

For a first-order theory $R$ extending ZFC, let $C_R$ be its set of formal consequences and let $\mathrm{Cons}$ denote the class of formal consistency statements $\mathrm{Con}(Q)$ for recursively axiomatized extensions $Q$ of ZFC. Using Gödel numbering to code proofs and theories, these objects and the following comparison are definable in the base theory ZFC.

The consistency-strength preorder isThus every consistency assertion provable in $T$ is also provable in $S$. Its strict part is

Let $\mathrm{IC}$ be the sentence asserting that a strongly inaccessible cardinal exists, and begin withDefine the iterated consistency progressionThe construction is effective, so every $T_n$ and $T_{\infty }$ is a recursively axiomatized first-order theory extending ZFC.

Because $T_{n+1}$ extends $T_n$, every theorem of $T_n$, including every formal consistency statement it proves, is a theorem of $T_{n+1}$; hence $T_n{\le }_{\mathrm{Cons}}{T}_{n+1}$. The theory $T_{n+1}$ proves $\mathrm{Con}(T_n)$ by construction, whereas a consistent $T_n$ cannot prove its own consistency by Gödel second incompleteness theorem. ThereforeLikewise $T_{\infty }$ extends every $T_n$ and contains $\mathrm{Con}(T_n)$ as an axiom already at stage $n+1$, while $T_n$ does not prove it. Consequentlyassuming the stated consistency hypotheses.

One-consistency says that no bounded arithmetic formula $F(x)$ has a provable existential closure while each of its standard numeral instances is refutable. It implies first-order consistency, since an inconsistent classical first-order theory proves every logical formula.

If $P$ is one-consistent, (i) gives $P⊬G$, so $a\notin D$. Numeralwise enumeration in arithmetic therefore givesIf $P⊢\neg G$, classical logic gives $P⊢\exists v_{2}A(\bar{a},v_2)$. The matrix is bounded, and the preceding displayed derivations refute every standard instance. This violates one-consistency. ConsequentlyTogether with (i), this yields undecidability of this first-order sentence under the stronger hypothesis, without asserting that ordinary first-order consistency alone suffices for its negative half.

Use the numeralwise enumeration in arithmetic convention in the first-order theory: membership supplies a standard stage with a provable enumerating instance, while nonmembership makes every standard-stage instance refutable. Put $D=\{n:P⊢E_n(\bar{n})\}$. By the definition of $a$, the diagonal instance $E_a(\bar{a})$ is exactly $G$.

If $P⊢G$, then $a\in D$. Numeralwise enumeration in arithmetic supplies a natural number $m$ such that $P⊢A(\bar{a},\bar{m})$. But universal instantiation of $G$ gives $P⊢\neg A(\bar{a},\bar{m})$. This contradicts first-order consistency. ThereforeThis uses the formal proof obligations in numeralwise enumeration in arithmetic in $P$, rather than merely the external assertion that a logical formula has a particular complexity.

Omega-consistency forbids a logical formula $B(x)$ of any complexity for which $S⊢\exists xB(x)$ and $S⊢\neg B(\bar{n})$ for every standard $n$. The difference from one-consistency is that the matrix is unrestricted. It implies first-order consistency.

For a complete first-order consistent classical first-order theory, theorem membership obeys the ordinary Boolean truth tables. For example, it proves a conjunction exactly when it proves both conjuncts; completeness and first-order consistency also make theoremhood of a negation the complement of theoremhood of the first-order sentence. Omega-consistency additionally gives the witness propertyThe reverse implication is existential introduction. For the forward implication, if no standard instance were provable, completeness would give a formal proof of each negated instance, violating omega-consistency. This works also after replacing additional free variables by numerals.

Now induct on logical formulas with their remaining free variables replaced by standard numerals. At the atomic level, the equivalence between theoremhood and standard truth follows from bounded completeness of an arithmetic theory and bounded soundness of an arithmetic theory from (b). The Boolean steps use the truth-table facts just proved. The existential step uses the witness property and the induction hypothesis on its matrix; universal quantification follows by negation. Hencefor every first-order sentence $X$. Completeness ensures it decides each first-order sentence, and this equivalence ensures every decision is correct.