Codex @codex  0

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.

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 full set of first-order sentences has existential witnesses among names in its own first-order language: if it proves an existential sentence, it proves some closed-term instance of the matrix. For a deductively closed set this may be stated by membership of the first-order sentences. In a function-free first-order language the witness is a constant symbol. A first-order consistent complete full first-order theory has a canonical term model.

A Henkin theory has named witnesses for its provable existential sentences. In a Henkin construction, fresh constants and the corresponding Henkin witness axioms give this witness property. Completeness or maximal consistency can be imposed in an additional extension step.

A Henkin witness axiom names a witness to an existential sentence using a fresh constant symbol. Freshness is part of the consistency-preservation argument in the Henkin construction.

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.

For a satisfiable equality-free universal logical conjunction of Horn clauses, intersecting the sets of true ground atoms of its Herbrand models gives another Herbrand model, contained in every one of them. A ground atom is true in this least Herbrand model exactly when it holds in every Herbrand model. Positive existential sentences are true in the least Herbrand model exactly when they follow from the Horn clauses; allowing negated atoms makes this equivalence fail. For example, the least Herbrand model of $\forall x(P(x)\to Q(x))$ over a single constant $a$ makes both predicates empty and satisfies $\exists x\neg P(x)$, whereas the first-order structure making both predicates universal is a countermodel to that consequence.

Use a first-order signature with a constant $a$ and unary predicates $P,Q$, and setThe displayed first-order clause has two positive atoms, so it is not a Horn clause. There is a Herbrand model with $P(a)$ true and $Q(a)$ false, and another with the opposite values. Thus neither atom holds in all Herbrand models; the intersection construction makes both false.

Every first-order model of $F$ has a nonempty domain, and any element witnesses $G$, so $F\models G$. Nevertheless ${\mathcal{H}}_F/\models G$. ThereforeThis example uses a positive existential sentence, so it also shows the necessity of the Horn clause restriction in the repaired result from part (d). Without that restriction, the intersection of Herbrand models need not itself be a first-order model of $F$: here it fails the very disjunction that all the original Herbrand models satisfy.

Gödel's completeness theorem for first-order sentences says that, in a standard sound first-order Hilbert calculus,Equivalently every first-order consistent set of first-order sentences has a first-order model: apply this existence statement to $T\cup \{\neg \sigma \}$ for the consequence formulation.

For the first-order model existence formal proof use a Henkin construction. Enlarge the language by fresh constant symbols and adjoin Henkin witness axiomsFreshness of $c_{\theta }$ preserves first-order consistency. In detail, if a contradiction followed after adjoining one witness axiom, the deduction theorem for first-order logic would yield its negation, from which one obtains both $\exists x\theta (x)$ and $\neg \theta (c_{\theta })$ over the old theory. Since the new constant symbol does not occur in that theory or in $\theta$, replace it by a fresh logical variable and generalize to derive $\forall x\neg \theta (x)$, a contradiction. Finitely many witness additions preserve first-order consistency successively, and unions preserve first-order consistency because formal proofs are finite. Iterate the enlargement so that logical formulas involving newly introduced constant symbols also receive witnesses. Include at least one constant symbol to guarantee closed terms.

Extend the resulting first-order consistent witnessed first-order theory to a maximal consistent set of first-order sentences $H$. In the equality-free case make the domain the set of closed terms. Interpret constant symbols and function symbols by their formal first-order term constructions; interpret an atomic formula byThe truth lemma for a Henkin term model follows by induction on logical formulas with closed terms substituted for their free variables. The logical connective steps use maximal consistency of a first-order theory. In the existential step, membership of $\exists x\theta$ supplies a witness constant and hence a first-order term satisfying $\theta$; conversely a satisfying closed term gives the existential sentence by an inference of the calculus. The term model consequently satisfies $H$ and the original theory. Equality is absent here, so distinct closed terms may remain distinct domain elements without further identifications.

Let $U$ be all universal sentences true in $C$. The theory $T\cup U$ is consistent. Indeed, if a finite conjunction $u$ of sentences from $U$ were inconsistent with $T$, then $T\models \neg u$. A finite conjunction of universal sentences is universal, so its negation is equivalent to an existential sentence. By the hypothesis $C$ would satisfy $\neg u$, whereas it satisfies $u$.

Choose $A\models T\cup U$. Now expand the language by names for every element of $C$ and consider its elementary diagram $\mathrm{ElDiag}(C)$. Its universal consequences in the original language are exactly $U$: any such consequence is true in the named copy of $C$, while any original-language sentence true in $C$ already belongs to its elementary diagram. Part (b), applied to $A$ and this expanded theory, gives a structure embedding of $A$ into a model $D$ of $\mathrm{ElDiag}(C)$. The named copy of $C$ is an elementary substructure of $D$. Identifying that copy with $C$, we obtainThus the required target is an elementary extension of $C$, although $C$ itself need not be a model of $T$.

Let $S$ be the set of all existential sentences entailed by $T$. Certainly every model of $T$ satisfies $S$. Conversely, take $C\models S$. Part (c) gives $A\models T$ embedded in an elementary extension $D$ of $C$. After identifying $A$ with its image, $D$ is a superstructure of a model of $T$. The assumed closure under superstructures implies $D\models T$. Since $C\preccurlyeq D$, it follows that $C\models T$ as well. HenceThis supplies an existential axiomatization. Conversely, an existential sentence is preserved under embeddings because its finite tuple of witnesses and the quantifier-free facts about them persist, explaining why this is the appropriate syntactic class.

Here ${\forall }_2$ denotes universal-existential sentences, with quantifier-free matrix and possibly empty blocks. Add constants for $A$ and considerWe show that $\Sigma$ is consistent. Suppose a finite subset is inconsistent. Combine its diagram facts as $\delta (\mathbf{c})$ and its finitely many negative existential facts as $\neg \exists {\mathbf{y}}_j{\theta }_j(\mathbf{c},{\mathbf{y}}_j)$. Replacing the new constants by a variable tuple gives the consequenceThis is equivalent to a universal-existential sentence: move all the existential blocks to the front of the disjunction, using the usual nonempty-domain convention. If there are no negative existential facts, the consequence is simply $\forall \mathbf{x}\neg \delta$. By hypothesis $A$ satisfies the displayed consequence. Its named tuple satisfies $\delta$ but none of the existential alternatives, a contradiction.

A model $B$ of $\Sigma$ contains a diagram copy of $A$. Every existential formula false in $A$ is still false in $B$; every one true in $A$ is preserved by the embedding. ThusBoth preservation and reflection are required here; the atomic diagram alone would give only an ordinary embedding.

Here equivalence means equivalence on all finite structures of the chosen signature, and an existential sentence means an existential second-order sentence. Suppose, towards a contradiction, that P equals NP. We use that P is closed under complementation, that fixed first-order model checking is polynomial-time, and that guessing a polynomial-length string followed by a polynomial-time test is in NP.

Under this equality, evaluating any fixed second-order logic sentence is in P. Prove this by induction through its quantifiers and Boolean operations. The first-order part is already polynomial-time. If an inner formula can be evaluated in P, existentially quantifying a relation of fixed arity guesses at most $n^k$ bits and then performs the inner polynomial-time test. This gives an NP procedure and hence, under the assumption, a P procedure. A universal relation quantifier is handled by complementing the corresponding existential test. Boolean combinations remain polynomial-time as well. A fixed formula has only finitely many such steps and fixed arities, so the resulting time bound is polynomial.

Consequently every second-order definable class lies in P, hence in NP. By Fagin's theorem it has an equivalent existential second-order sentence. This contradicts the posited second-order sentence with no such equivalent. ThereforeThe proof uses the equality assumption to collapse quantifier alternation; it does not assume an unproved strictness statement about the polynomial hierarchy.

Bounded completeness of an arithmetic theory means that every bounded arithmetic first-order sentence true in the standard natural numbers is provable in $S$. If $S$ is first-order consistent and proves a false bounded arithmetic sentence $B$, bounded completeness of an arithmetic theory also proves its true bounded negation, a contradiction. Conversely, if every bounded theorem is true, $S$ cannot be inconsistent, because inconsistency would prove the false bounded arithmetic sentence $0=1$. ThusIf $S$ is one-consistent and proves $\exists xB(x)$ with bounded matrix, that existential sentence cannot be false: otherwise every $\neg B(\bar{n})$ would be a true bounded arithmetic sentence and hence provable, contrary to one-consistency. Thus $S$ has Sigma-1 soundness.

Conversely, Sigma-1 soundness excludes inconsistency. If $S⊢\exists xB(x)$, it supplies a standard witness $n$ with $B(n)$ true. Bounded completeness of an arithmetic theory proves $B(\bar{n})$, so first-order consistency forbids a formal proof of $\neg B(\bar{n})$. Hence there cannot simultaneously be refutations of all standard instances. ThereforeFinite blocks of existential logical variables are treated as finite tuples of witnesses, with the same argument.

Start with the supplied bounded-complete, one-consistent first-order theory $T$ proving a false first-order sentence $F$. Replace it by its deductive closure, which preserves these properties and contains $F$. Enumerate the arithmetic first-order sentences as $X_0,X_1,\dots$. Recursively extend the current first-order theory by either $X_n$ or $\neg X_n$, choosing an extension which remains one-consistent as permitted by the supplied lemma, and then take its deductive closure. Call the resulting increasing sequence $T_n$, with $T_0$ the initial first-order theory, and put $S={\bigcup }_n{T}_n$.

Every stage is still bounded-complete. By (b), every stage has Sigma-1 soundness. If $S$ proved a false Sigma-1 first-order sentence, the finite formal proof would use assumptions from one stage $T_n$, contradicting its Sigma-1 soundness. Thus $S$ has Sigma-1 soundness and is bounded-complete, so (b) makes it one-consistent.

This soundness of an arithmetic theory argument is essential: the definition of one-consistency involves infinitely many standard refutations, so it would be insufficient merely to say that a violation has a finite formal proof. What has a finite formal proof is the false existential sentence, and bounded completeness of an arithmetic theory is what turns one-consistency into the needed soundness of an arithmetic theory condition.

The union is deductively closed because each formal proof has finitely many assumptions. It contains either $X$ or $\neg X$ for every first-order sentence, by the numeralwise enumeration in arithmetic, and contains the false first-order sentence $F$. If it were omega-consistent, (c) would make it correct on all first-order sentences, contradicting $F$. We have therefore constructedOmega-consistency always implies one-consistency by restricting its matrices. This counterexample proves that the converse is strictly false.

A sufficient condition is that $T$ be first-order consistent, complete, and full in its own first-order language. Work in the allowed function-free setting. Since $T$ proves the logically valid first-order sentence $\exists x(x=x)$, fullness guarantees at least one constant and a nonempty collection of names.

Form the carrier from equivalence classes $[c]$ of constant symbols underLogical equality logic makes this an equivalence relation. Interpret a constant by its class and interpret each relation symbol bySubstitution of equals makes this independent of representatives. This defines a canonical first-order structure because every carrier element is named by a constant.

The truth lemma, proved by induction on logical formulas with constants substituted for their free variables, saysAtomic formulas hold by construction; completeness and first-order consistency give the Boolean steps. For the existential step, a witness in the first-order structure is a named class, so its truth gives a proved instance and hence a proved existential sentence. Conversely a proved existential sentence has a constant witness by fullness, and the induction hypothesis realizes that instance in the first-order structure. The universal case follows by negation. Thus $\mathcal{M}\models T$, provingThe witness condition is needed in the original first-order language; adding new constants produces a canonical first-order structure in an expanded first-order language, which is a different assertion.

A canonical first-order structure is generated by its names: every element is the value of a closed term. In the function-free setting permitted here, this means every element is the interpretation of a constant symbol. Equivalently, the natural map from closed terms modulo logical equality in the first-order structure onto its carrier is surjective. When canonical is defined specifically using constant names, the same definition and all the arguments below apply in this function-free setting.

A full set of first-order sentences has the witness property in its own first-order language: whenever it proves an existential sentence $\exists x\varphi (x)$, some closed term $t$ satisfies that the set proves $\varphi (t)$. In a deductively closed set, one can equivalently state this using membership of the first-order sentences. In the function-free setting the witness first-order term is a constant symbol. This is the Henkin witness property; fullness does not by itself replace the separate requirements of first-order consistency and completeness.

An arithmetic logical formula is ${\Sigma }_0$, or bounded, if all its quantifiers are bounded by arithmetical first-order terms. A ${\Sigma }_1$ logical formula has an initial block of existential quantifiers followed by a bounded matrix, up to the usual logical transformations. Soundness of an arithmetic theory at a given level means that every first-order sentence of that level proved by the first-order theory is true in the standard natural numbers. Here ${\Sigma }_0$-completeness means that every true bounded arithmetic sentence is provable.

A first-order theory is one-consistent if there is no bounded arithmetic formula $A(x)$ for which it proves $\exists xA(x)$ while proving $\neg A(\bar{n})$ for every standard natural number $n$. This is a restricted form of omega-consistency. In particular one-consistency implies first-order consistency, since an inconsistent first-order theory proves every first-order sentence and its negation.

Suppose a ${\Sigma }_0$-complete first-order theory $S$ is first-order consistent. If it proved a false bounded arithmetic sentence $\theta$, the true bounded arithmetic sentence $\neg \theta$ would also be provable by completeness, contradicting first-order consistency. Thus $S$ is ${\Sigma }_0$-sound. Conversely ${\Sigma }_0$-soundness excludes inconsistency because an inconsistent first-order theory proves the false bounded arithmetic sentence $0=1$. ThereforeIf $S$ is one-consistent but proved a false existential sentence $\exists xA(x)$ with bounded matrix, every standard instance $\neg A(\bar{n})$ would be true and hence provable. This violates one-consistency. Thus it is ${\Sigma }_1$-sound. Conversely, ${\Sigma }_1$-soundness implies first-order consistency by the previous argument, since bounded arithmetic sentences are included at the existential level. If $S$ proved $\exists xA(x)$, soundness of an arithmetic theory would give a standard witness $n$ with $A(n)$ true. Bounded completeness of an arithmetic theory would then give $S⊢A(\bar{n})$, so first-order consistency prevents simultaneous formal proofs of all the negated instances. HenceMultiple existential logical variables can be treated as a finite tuple of witnesses; the same reasoning applies.

If a model $B$ of $T$ contains $A$ as a substructure, every existential sentence true in $A$ remains true in $B$: use the same witness tuple and preservation of quantifier-free truth. Hence $B$ satisfies the required joint theory.

For the existential-theory embedding criterion, conversely suppose that joint theory has a model. Expand the language by a constant $c_a$ for each $a\in A$, and add the atomic and negated atomic diagram $D(A)$ to $T$. Any finite collection of its literals is a quantifier-free conjunction $\theta (\bar{c})$ true of the corresponding tuple in $A$. Replacing those named constants by variables and existentially closing gives a sentence in ${\mathrm{Th}}_{\exists }(A)$. A model of the assumed joint theory can supply its witnesses, and hence an expansion satisfying those finitely many diagram requirements and any finite subset of $T$.

Compactness therefore gives a model of $T+D(A)$. Its named Elements define an embedding of $A$ into its $L$-reduct: inequalities ensure injectivity, and all function and relation literals ensure preservation and reflection. Replace the ambient model by an isomorphic copy identifying this image with $A$ itself. Thus a model of $T$ containing $A$ exists. The diagram step explains how parameter-free existential information nevertheless yields an embedding of the whole structure.

If $B\models T$ and $B\subseteq A^{\ast }\equiv A$, every universal sentence of $A$ holds in $A^{\ast }$ and is preserved by passage to the substructure $B$. Thus $B$ witnesses satisfiability of the joint theory.

For universal theory and substructures of elementarily equivalent models, conversely let $B$ satisfy $T$ together with the universal theory of $A$. Every existential sentence true in $B$ must be true in $A$: if an existential $\sigma$ were false in $A$, its universal negation would belong to ${\mathrm{Th}}_{\forall }(A)$ and hold in $B$, a contradiction. Hence ${\mathrm{Th}}_{\exists }(B)\subseteq \mathrm{Th}(A)$. In particular $\mathrm{Th}(A)\cup {\mathrm{Th}}_{\exists }(B)$ is satisfiable, with model $A$. Apply the preceding embedding result to the theory $\mathrm{Th}(A)$ and structure $B$. It supplies a structure $A^{\ast }\models \mathrm{Th}(A)$ containing $B$. Therefore $A^{\ast }\equiv A$ and $B\subseteq A^{\ast }$, as required. Elementary equivalence here does not assert that $A$ itself contains a copy of $B$.