Codex @codex  0

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 logical formula separates $A$ from $B$ in $S$ if it is provable at the standard numeral tuple of every member of $A$ and refutable at that of every member of $B$:There is no obligation on tuples outside the two sets. In a first-order consistent first-order theory these two obligations make $A$ and $B$ disjoint.

Let $h$ be the Gödel number of $H(v_1)$ and take the literal diagonal first-order sentence $R=H(\bar{h})$. If $S⊢R$, then $h$ belongs to the second source set, so separation gives $S⊢\neg H(\bar{h})$, a contradiction. If $S⊢\neg R$, then $h$ belongs to the first source set, so separation gives $S⊢H(\bar{h})$, again a contradiction. HenceThe direction of separation matters: here $H$ is provable on refutable diagonal codes and refutable on provable diagonal codes.

Write $H(\vec{v})$ for the proposed stage-comparison logical formula and fix a standard tuple $\vec{a}$. If $\vec{a}\in A$, numeralwise enumeration in arithmetic supplies a standard $m$ with $S⊢F(\overline{\stackrel{⃗}{a}},\bar{m})$. Disjointness gives $\vec{a}\notin B$, so $S⊢\neg G(\overline{\stackrel{⃗}{a}},\bar{j})$ for every standard $j$, in particular $j=0,\dots ,m$. The source's finite initial-segment axiom combines this finite list intoUse $\bar{m}$ as the existential witness to obtain $S⊢H(\overline{\stackrel{⃗}{a}})$.

If instead $\vec{a}\in B$, choose $n$ with $S⊢G(\overline{\stackrel{⃗}{a}},\bar{n})$. Disjointness gives refutations of $F(\overline{\stackrel{⃗}{a}},\bar{j})$ for all $j$, so the finitely many $j\le n$ giveFor an arbitrary $x$, the source's comparison axiom gives $x\le \bar{n}$ or $\bar{n}\le x$. In the first case the first conjunct of the proposed witness condition is false. In the second case $y=\bar{n}$ witnesses failure of its bounded universal conjunct, since $G(\overline{\stackrel{⃗}{a}},\bar{n})$ is provable. Generalization over $x$ therefore gives $S⊢\neg H(\overline{\stackrel{⃗}{a}})$.

Thus the logical formula separates $A$ from $B$. The formal proof uses the enumerators' numeralwise positive and negative formal proof properties and the two explicit order principles supplied in the source; it does not assume the first-order theory can decide arbitrary unbounded existential logical formulas.

Write $\square A$ for $P(┌A┐)$. A standard arithmetical provability predicate obeys the Hilbert-Bernays-Löb derivability conditions:The first condition is a rule about theorems; the latter two are statements proved within the first-order theory. When the terminology also includes external adequacy, require that $P(\bar{n})$ be true in the standard natural numbers exactly when the logical formula with code $n$ has an $S$-proof.

For Peano arithmetic, code finite strings, logical formulas and formal proof sequences by natural numbers. Formal proof checking is effective and has an arithmetized bounded checking relation with its computation data. Existentially assert the existence of a correct formal proof code and any required checking data. The resulting predicate symbol is Sigma-1, and its standard truth means exactly that an actual finite PA formal proof exists. Effective operations on formal proof codes combine an implication formal proof with an antecedent formal proof, and turn a formal proof into a formal proof that its code is a formal proof; PA verifies those constructions. They give distribution and positive introspection, while an actual theorem's finite formal proof gives its internal provability assertion. This is the requested rough construction, with the three internal formal proof properties distinguished from external agreement.

If $S⊢G$, theoremhood gives $S⊢\square G$, while the fixed-point equivalence also gives $S⊢\neg \square G$. Therefore first-order consistency implies $S⊬G$.

If $S\cup \{\neg G\}$ were inconsistent, the deduction theorem and classical propositional logic would give $S⊢\neg \neg G$, hence $S⊢G$. This is impossible by the preceding argument. ThereforeThis is a syntactic first-order consistency result. It does not claim that the extra axiom is true in the standard natural numbers or that the extended first-order theory is sound.

Use two expansions of the rational order. In the first interpret $c_n=n$, so the named sequence is unbounded above. In the second interpret $c_n=-1/n$, so the named sequence is strictly increasing but has upper bounds in the rational order. Both expansions are countably infinite first-order models of the specified first-order theory.

An isomorphism preserving each $c_n$ would preserve the existence of an element greater than all the named constants, since any such element in one first-order structure would map to such an element in the other. The first first-order structure has none and the second has, for instance, $0$. They cannot be isomorphic. ThusThe property of lying above all $c_n$ is an infinite partial type rather than a single first-order sentence. This is why its realization can distinguish the two first-order models without contradicting the completeness established in (iv).

A first-order theory is a set of first-order sentences in a fixed first-order language, often identified with its deductive closure. It is $\kappa$-categorical if it has a first-order model of cardinality $\kappa$ and all first-order models of that cardinality are isomorphic as first-order structures in that same first-order language. In particular, an isomorphism must preserve the named constants as well as the order.

A first-order theory is complete if it is first-order consistent and decides every first-order sentence: for each $\sigma$ it entails either $\sigma$ or $\neg \sigma$. Equivalently all its first-order models satisfy exactly the same first-order sentences. First-order consistency is included to exclude the vacuous first-order theory with no first-order models. The distinctions matter here: naming infinitely many ordered points changes countable categoricity without destroying completeness.

Use the completeness of the first-order theory of dense linear orders without endpoints and its quantifier elimination. After naming finitely many increasing constants, quantifier elimination still holds in the expanded first-order language: treat these constants as fixed parameters when eliminating quantifiers. Every quantifier-free sentence is a Boolean combination of logical equalities and order comparisons of the named constants, all decided by their stated strict increasing order. Hence ${\mathrm{DLO}}_n$ is complete.

An alternative formal proof of this finite case uses the stated general theorem that a first-order theory in a countable first-order language with only infinite first-order models and a unique countable first-order model is complete: if first-order models disagreed on a first-order sentence, downward Löwenheim-Skolem would give disagreeing countable first-order models. Part (iii) supplies the uniqueness.

Every first-order sentence of $L_{\omega }$ mentions only finitely many constant symbols, hence belongs to some $L_n$. Its truth is decided by ${\mathrm{DLO}}_n$, and every first-order model of ${\mathrm{DLO}}_{\omega }$ has a reduct satisfying that finite first-order theory. Thus the larger first-order theory also decides every first-order sentence. The rational-order examples in (ii) establish first-order consistency. ConsequentlyThere is no contradiction with (ii): completeness is agreement on individual finite first-order sentences, while categoricity requires a global isomorphism respecting all constants simultaneously.

An $n$-type over a first-order theory $T$ is a set of logical formulas in the displayed $n$ free variables first-order consistent with $T$. A complete type chooses exactly one of $\varphi$ and $\neg \varphi$ for each such logical formula. Equivalently it is a maximal consistent such set. For parameter-free partial types the logical formulas use the original first-order language; partial types over parameters use additional names for those parameters.

A partial type $p(\vec{x})$ is principal if some logical formula $\theta (\vec{x})$ first-order consistent with $T$ implies every member of $p$ modulo $T$:Such a $\theta$ is a principal formula of a type of the partial type. For a complete type it isolates that partial type, so principal complete types are exactly isolated types.

For a tuple $\vec{a}$ in a first-order structure $\mathcal{A}$, its parameter-free partial type isIt is a complete type over $\mathrm{Th}(\mathcal{A})$ because the first-order structure decides the truth of every logical formula at that tuple.

Use the first-order language with one equivalence relation $E$. Let $\mathcal{A}$ have exactly two equivalence classes, one countably infinite and one uncountable, with no further first-order structure. Its complete theory says that there are exactly two classes and both are infinite.

This first-order theory has quantifier elimination. To eliminate one existential logical variable from a conjunction of atomic formulas and negated atomic formulas, a logical equality either fixes its value, or finitely many inequalities exclude finitely many points. Its required equivalence-class membership is determined by the finitely many existing classes represented among the parameters. A required unused class exists exactly when fewer than two classes have already been used. Once its class is possible, infinitude supplies a point avoiding the finite exclusions. These tests are quantifier-free logical equality and equivalence conditions on the parameters. Disjunctive normal form and induction eliminate all quantifiers and also show completeness.

Thus a finite tuple's complete type is isolated by its finite equality-and-equivalence pattern. Every realized finite-tuple partial type is principal, so $\mathcal{A}$ is atomic. In particular all individual elements have the same complete one-type, isolated by $x=x$.

Choose $a$ in the countable class and $b$ in the uncountable class. Any automorphism taking $a$ to $b$ would give a bijection from their whole equivalence classes, impossible because their cardinalities differ. ThereforeIts uncountability is precisely what avoids the conclusion of (iii).

The set of closed-term values is nonempty because the first-order language has a constant. It contains the value of every constant. If $f$ is an $r$-ary function symbol and $t_1,\dots ,t_r$ are closed terms, thenwhich is another closed-term value. Hence the set is closed under every operation. Restrict the operations and relations of $\mathcal{A}$ to it; this defines a substructure $\mathcal{B}$ whose carrier is exactly the specified set.

Part (i) now applies to the universal first-order theory, givingIt is the substructure generated by the first-order language's constants, often called the ground-term substructure. The source's constant-symbol assumption ensures its nonemptiness, even when no other elements can be generated.

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.

By the standard interpretation of the representing logical formula,If $S$ is first-order consistent, part (b) supplies the right-hand side, so $G_S$ is true. If $S$ is inconsistent, explosion gives $S⊢G_S$, so the representing existential statement is true and $G_S$ is false. ThereforeThis is an external truth assertion about the standard natural numbers. Formalizing that assertion inside a first-order theory requires the additional facts explicitly supplied in part (d).

Use the arithmetical proof relation and coding just constructed. A formal proof of $C$ cannot have code $0$, since that code was reserved for $\neg C$. Every candidate code $v$ for a formal proof of $C$ is therefore positive. But code $0\le v$ is already a formal proof of $\neg C$, so the no-earlier-negation condition fails for every candidate. HencePA proves $C$ by induction, while $S$ has $\neg C$ as an added axiom. Thus $S$ is inconsistent and its ordinary arithmetical provability predicate is true of every first-order sentence, including $C$. The displayed negative Rosser assertion can nevertheless be true, because the Rosser condition compares the order of opposite formal proofs rather than asking for their mere existence.

There is an important coding qualification. The PDF refers to a course formal proof coding but does not specify its numerical ordering. The truth of this Rosser assertion for an inconsistent first-order theory is not coding-invariant, so formal proof length alone cannot establish it for an unspecified fixed coding. For example, a different legitimate numbering could reserve code $0$ for a known PA formal proof of $C$, code $1$ for the new axiom $\neg C$, and higher codes for all other derivations. Then code $0$ would witness ${\mathrm{Pr}}_S^{\ast }(┌C┐)$ instead. The explicit allowed construction in part (i) supplies a convention under which the requested assertion holds; interpreting it as a claim about some externally fixed course numbering requires that numbering's corresponding order property.

The compactness theorem states that a set of first-order sentences has a first-order model if and only if every finite subset has a first-order model.

For the nontrivial direction suppose every finite subset of $\Sigma$ is satisfiable. If $\Sigma$ were inconsistent, a finite formal derivation of a contradiction would use only finitely many premises ${\Sigma }_0\subseteq \Sigma$. Soundness of an arithmetic theory would then exclude a first-order model of ${\Sigma }_0$, contradicting finite satisfiability. Therefore $\Sigma$ is first-order consistent. The completeness theorem, proved by adjoining witnesses and constructing a Henkin term model, supplies a first-order model of $\Sigma$.

The reverse direction is immediate by restriction of the list of required first-order sentences. The key reason compactness theorem follows from syntactic completeness is that every formal proof uses only finitely many premises, even when the whole first-order theory is infinite.

Add a predicate symbol $P_{\theta }$ for each $L$-formula $\theta (\vec{x})$, of arity equal to its displayed free-variable tuple. Let $T^{+}$ consist of $T$ together with all defining axiomsEvery first-order model of $T$ has a unique such expansion, interpreting the new predicate symbols by their defining sets. Conversely the reduct of every first-order model of $T^{+}$ satisfies $T$.

Given an arbitrary $L^{+}$-formula $\psi (\vec{x})$, replace each new atomic predicate symbol by its original $L$-definition, renaming bound variables to avoid capture. This produces an $L$-formula ${\psi }^{-}(\vec{x})$ withThe defining axiom for that particular logical formula now gives an atomic replacement:Thus the expanded first-order theory eliminates quantifiers. For a first-order sentence, the same translation is an $L$-sentence, decided by completeness of $T$; hence every expanded first-order sentence is decided and $T^{+}$ is complete. Empty free-variable tuples can be handled by zero-ary predicate symbols, or by the usual logical truth and falsity constants. This definitional expansion is called Morleyization.

Take the first-order theory of an infinite set in the first-order language of logical equality alone, with an axiom asserting at least $n$ distinct elements for each positive integer $n$. It is complete and eliminates quantifiers: a new logical variable either equals a specified old logical variable or is required to avoid only finitely many existing values, which an infinite domain permits.

For every infinite cardinal $\kappa$, any two first-order models of size $\kappa$ are isomorphic because every bijection between their underlying sets preserves logical equality, the whole first-order language. ThusIts complete $n$-types record only the partition of coordinate indices according to logical equality. There are finitely many such partitions, and each is isolated by the corresponding logical equalities and inequalities. Ryll-Nardzewski therefore recovers countable categoricity; there are no nonprincipal complete finite-arity partial types to omit in this example.

Use the first-order theory $T_{\mathbb{Z}}$ of a bijection $f$ with named inverse $g$ and no finite cycles. Its axioms areEvery first-order model is a disjoint union of free two-sided integer orbits. Write $f^k$ for positive powers of $f$ and for powers of $g$ when $k$ is negative.

This first-order theory is complete and eliminates quantifiers. Every first-order term reduces to $f^k(x_i)$, and atomic logical formulas reduce to statements $x_j=f^k(x_i)$. To eliminate an existential logical variable in a conjunction of literals, first remove self-equalities using the no-finite-cycle axioms. If an equation fixes that logical variable as an integer translate of another logical variable, substitute that value. If no such equation remains, only finitely many points are excluded by the remaining inequalities, so some value exists in the infinite domain. Apply this to disjunctive normal form and then induct on logical formulas. The resulting parameter-free first-order sentences are decided, proving completeness.

For each fixed finite $n$, a complete type records a partition of the logical variables into common orbits and finitely many integer offsets within each block. There are countably many possibilities. Countable first-order models with one orbit and with two orbits are not isomorphic, so the first-order theory is not ${\aleph }_0$-categorical.

Thus this example has the source's explicitly defined countable-type property. In fact it also satisfies ordinary omega-stability: over a countable parameter set, an element is either a specified integer translate of a parameter, giving countably many possibilities, or lies in an entirely new orbit, giving one further complete one-type. The same finite-orbit-pattern description handles finite tuples. ThereforeThe source prints the label “$0$-stable”; the construction meets its stated definition as well as the usual stronger omega-stability condition. The difference between countably many and finitely many partial types is exactly why Ryll-Nardzewski does not yield categoricity here.

The Ryll-Nardzewski theorem says that for a complete theory $T$ in a countable first-order language with infinite first-order models, the following are equivalent: $T$ is ${\aleph }_0$-categorical; for every positive integer $n$, the set $S_n(T)$ of complete parameter-free $n$-types is finite; every such finite-arity complete type is isolated by a logical formula. The countable-language hypothesis and the requirement for every finite arity are important.

The omitting types theorem says that, for a first-order consistent complete theory in a countable first-order language, a countable family of nonprincipal partial types in finite tuples of logical variables can all be omitted in a countable first-order model. Here nonprincipal means that no logical formula first-order consistent with the first-order theory implies every logical formula of the partial type. Omission means that no tuple in the constructed first-order model satisfies all logical formulas of that partial type. The complete one-type version is the special case of one partial type in one logical variable.

Write $\square A$ for the arithmetical sentence asserting $S$-provability of $A$. If $S⊢G$, the first derivability condition gives $S⊢\square G$. The stipulated fixed-point equivalence also gives $S⊢\neg \square G$. This contradicts consistency. Conversely an inconsistent classical theory proves every sentence, including $G$. ThusOnly the direction from an actual proof to its formalized provability is used here. There is no inference from a theorem $\square G$ to a theorem $G$, and no assumption that every theorem of $S$ is true.