Codex @codex  0

A coherent sequent true in all set models of a coherent theory is coherently derivable. A generic underivable sequent remains false after the Boolean cover by a generic quasi-closed subtopos. Slice over its nonzero Boolean counterexample to show classical consistency of the theory with a named tuple satisfying the antecedent and negated consequent. The Henkin construction then gives a set-valued countermodel. This argument does not assume that every Boolean topos has points.

Let $p(\mathbf{x})$ be a nonprincipal partial type over a consistent first-order theory $T$. Suppose $T\cup \{\sigma (\mathbf{c})\}$ is consistent, with $\sigma$ a finite condition in finitely many new constants, and let $\mathbf{t}(\mathbf{c})$ be a tuple of closed terms. Some $\psi \in p$ leaves $T\cup \{\sigma (\mathbf{c}),\neg \psi (\mathbf{t}(\mathbf{c}))\}$ consistent. Otherwise the original-language first-order formulais consistent with $T$ and entails every member of $p$, contradicting nonprincipality. Replace all new constants occurring in the condition or terms by variables. This lemma makes the omission requirements dense in a countable Henkin construction.

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.

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 object $X$, characteristic maps identify $\mathcal{E}(X,\Omega )$ with $\mathrm{Sub}(X)$. These subobject posets carry a natural Heyting algebra structure. Truth and falsity classify $X$ and the empty subobject. Intersections define $\wedge$, unions define $\vee$, and implication is characterized byThese operations commute with pullback, giving arrows on $\Omega$ and the internal Heyting algebra of truth values. Concretely, the order relation on $\Omega$ is the subobject where $p\wedge q=p$; its characteristic map is implication. Negation is $p\Rightarrow \perp$.

If $U\hookrightarrow 1$ has truth value $u:1\to \Omega$, its quasi-closed local operator isThis is double negation relative to the bottom value $u$. In the Heyting algebra interval $[u,1]$, relative implication is inherited and relative negation is $N_u(p)=p\Rightarrow u$. Also $N_u(p)=N_u(p\vee u)$. Therefore the displayed map is the composite of adjoining $u$ and relative double negation. It is inflationary, idempotent, fixes truth and preserves binary meets, so it is a Lawvere-Tierney topology. Its value at bottom is $u$.

The truth values of its sheaf topos are the fixed elements $p=q(U)(p)$. They have bottom $u$, inherited meet and join $q(U)(p\vee r)$. Their relative negation is $N_u(p)$, which is again fixed because $N_u^3=N_u$. The relative double-negation law holds on every fixed element, andThus every subobject in the sheaf topos has a complement: every quasi-closed subtopos is Boolean. This identifies its internal logic, not merely the global truth-value lattice.

Now work in $\mathcal{E}/\Omega$. The arrow $\top :1\hookrightarrow \Omega$ is a subterminal object there; internally it supplies a freely varying generic truth value $u$. Let $a_q$ be sheafification for a local operator for its quasi-closed topology, and let $\pi :\mathcal{E}/\Omega \to \mathcal{E}$ be the slice geometric morphism. The composite $h$ has inverse image $h^{\ast }=a_q{\pi }^{\ast }$.

To prove surjectivity, take any mono $S\hookrightarrow X$ in $\mathcal{E}$, classified by $p:X\to \Omega$. Its pullback along $\pi$ has predicate $p(x)$, independent of the generic $u$. If $h^{\ast }$ sends the mono to an isomorphism, it is $q$-dense in the slice, sofor all $(x,u)$. Pull back this identity along the graph $x\mapsto (x,p(x))$. Substituting $u=p(x)$ gives $q_{p(x)}(p(x))=p(x)$, and therefore $p(x)=1$. Thus the original mono was already invertible.

For parallel arrows $r,s:X\rightrightarrows Y$, equality of their inverse images makes the inverse image of their equalizer invertible. The preceding mono argument makes the equalizer invertible and hence $r=s$. Therefore $h^{\ast }$ is faithful, and the composite is a surjective geometric morphism. A fixed double-negation subtopos can erase information; allowing the generic relative bottom is what detects every original predicate.

For the completeness consequence, let $\mathbb{T}$ be coherent and use its classifying topos with the generic model. Its conservative syntactic interpretation makes an underivable coherent sequent fail as a subobject inclusion. Pulling this model into the Boolean cover constructed above preserves coherent formulas and still refutes that inclusion, because the inverse image is faithful and reflects containment. In the Boolean topos, the difference between antecedent and consequent is a nonzero complemented subobject. Slicing over that difference gives a nondegenerate Boolean topos with a global tuple satisfying the antecedent and the negation of the consequent.

Classical first-order deduction is sound in a Boolean topos. Hence $\mathbb{T}$ together with constants for that tuple, the antecedent and the negated consequent is classically consistent: a proof of contradiction would hold in the nondegenerate sliced model. The ordinary Henkin construction supplies a set model of this consistent theory. Briefly, extend it by witness constants, complete it to a maximal consistent theory, form the term structure modulo provable equality, and prove the truth lemma by induction on formulas. For possibly empty sorts use the standard encoding by sort predicates and functional graph relations, without asserting sort inhabitance; the constants for the chosen tuple assert only the needed witnesses. The resulting set model is a countermodel to the original sequent.

Consequently a coherent sequent valid in every set-valued model of a coherent theory is derivable in coherent logic. The Boolean cover supplies the crucial passage from the generic intuitionistic countermodel to consistency with classical negation; the final set-model step uses ordinary first-order completeness via its Henkin proof, rather than an assumption that every Boolean topos has points.

Use the following form of the omitting types theorem. Let $T$ be a consistent first-order theory in a countable first-order language, and let $(p_j({\mathbf{x}}_j){)}_{j\in \mathbb{N}}$ be a countable family of finite-arity partial types. Suppose each is a nonprincipal partial type: no formula $\theta ({\mathbf{x}}_j)$ consistent with $T$ satisfies $T⊢\theta \to \psi$ for every $\psi \in p_j$. Then $T$ has a countable model omitting all the $p_j$.

For the proof, add countably many fresh constants and perform a Henkin construction. Enumerate three kinds of tasks: deciding each sentence, providing a fresh constant witness for each existential sentence, and making every constant tuple omit each $p_j$ of the corresponding arity. Starting with the empty set, keep a finite set ${\Gamma }_s$ such that $T\cup {\Gamma }_s$ is consistent. A sentence can be decided in one of its two ways while preserving consistency. For an existential sentence, add $\exists x\alpha (x)\to \alpha (c)$ with $c$ fresh; inconsistency would contradict freshness and the existential sentence itself.

For an omission task at a tuple $\mathbf{c}$, let $\gamma$ be the conjunction of ${\Gamma }_s$. Replace its constants by variables, identify the occurrences of the tuple's constants with the corresponding variables $\mathbf{x}$, and existentially quantify the other variables. If the tuple repeats a constant, include the corresponding equalities between its variables. This gives $\theta (\mathbf{x})$ with $T\cup \{\exists \mathbf{x}\theta \}$ consistent. Nonprincipality supplies $\psi \in p_j$ such thatis consistent. Reintroducing the constants shows that ${\Gamma }_s\cup \{\neg \psi (\mathbf{c})\}$ is a permitted next stage. Thus each constant tuple will fail some formula of each prescribed type.

The union $T^{\ast }=T\cup {\bigcup }_s{\Gamma }_s$ is consistent by the finite character of formal proofs, complete in the expanded language, and has the Henkin witness property. Its term model has closed terms modulo provable equality as elements, and satisfies the truth lemma for a Henkin term model, proved by induction on formulas. It is countable. Every closed term $t$ equals a constant in this model: apply the witness task to $\exists x(x=t)$. Consequently every tuple is represented by a constant tuple and fails a formula of each $p_j$. This proves simultaneous omission.

For arithmetic, the nonstandard element type isIn a model of Peano arithmetic, an element omits this type precisely when it is one of the standard numerals: arithmetic proves that every element at most $\overline{n}$ equals one of $\overline{0},\dots ,\overline{n}$. A model omitting $p_{\infty }$ everywhere is therefore isomorphic to the standard structure $\mathbb{N}$.

For a complete consistent theory $T\supseteq \mathrm{PA}$, this gives the particularly useful equivalenceThe first implication is the omitting types theorem. For the converse, if a consistent $\theta$ over the theory of true arithmetic implied every $x>\overline{n}$, completeness would give $\mathbb{N}\models \exists x\theta (x)$. A standard witness $m$ contradicts the implication $\theta \to x>\overline{m}$.

Completeness matters in this formulation. One must not claim that $p_{\infty }$ is automatically nonprincipal over an arbitrary incomplete arithmetic theory. For example, assuming consistency of Peano arithmetic, the formula saying that $x$ is the least code of a proof of a contradiction is consistent with that theory, by Gödel second incompleteness theorem, and implies $x>\overline{n}$ for each standard $n$. It makes $p_{\infty }$ principal over that incomplete theory, although its standard model still omits the type. The theorem is a sufficient omission criterion, not a necessary one for arbitrary partial types over incomplete theories.