Codex @codex  0

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 tha first-order consistency.

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.

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.

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.

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.

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.

The definition of $a$ makes the diagonal instance $E_a[\bar{a}]$ exactly $G_S$. The representing logical formula therefore has the standard interpretationIf $S⊢G_S$, choose an actual witness $m$ to the left-hand existential statement. The bounded arithmetic sentence $A(\bar{a},\bar{m})$ is true and hence provable by ${\Sigma }_0$-completeness. But $G_S$ also gives $S⊢\neg A(\bar{a},\bar{m})$, a contradiction. ThusNow assume one-consistency. It implies first-order consistency, so no formal proof of $G_S$ exists and $A(a,m)$ is false for each standard $m$. Each bounded arithmetic sentence $\neg A(\bar{a},\bar{m})$ is consequently true and provable. A formal proof of $\neg G_S$ would give a formal proof of $\exists v_{2}A(\bar{a},v_2)$ while every standard witness instance is refuted, contrary to one-consistency. HenceThe two hypotheses play different roles: ordinary first-order consistency excludes the positive Gödel sentence, while the stronger hypothesis also excludes its negation.

Put $T=S\cup \{\neg G_S\}$. The first supplied equivalence, retained in $T$, combines with its new axiom to giveThe supplied implication $\mathrm{Con}(T)\to \mathrm{Con}(S)$ then yields, by contraposition,Finally the second supplied equivalence is $T⊢G_T\leftrightarrow \mathrm{Con}(T)$, so propositional reasoning givesNo extra first-order consistency assumption is needed for this formal derivation. If $S$ is first-order consistent, part (b) shows that adding $\neg G_S$ preserves first-order consistency, because inconsistency of the extension would imply $S⊢G_S$. Such a first-order consistent extension therefore proves the negation of its own true Gödel sentence, illustrating why first-order consistency alone does not imply one-consistency.

Write $\rho ={\mathrm{Pr}}_{PA}^{\ast }(┌R┐)$. The supplied fixed-point equivalence gives $PA⊢R\leftrightarrow \neg \rho$.

If PA proved $R$, the first assumed property would give $PA⊢\rho$, while the equivalence would give $PA⊢\neg \rho$. This contradicts first-order consistency. If PA proved $\neg R$, the second assumed property would give $PA⊢\neg \rho$, and the reverse implication of the equivalence would give $PA⊢R$, again a contradiction. HenceThis is the Rosser improvement: its comparison of formal proof codes permits ordinary first-order consistency to exclude both alternatives, without assuming one-consistency.

Use the two formal consistency equivalences expressly supplied for this part. If $S⊢G\leftrightarrow R$, the derivability conditions give $S⊢\square \neg G\leftrightarrow \square \neg R$. Taking negations and applying those supplied equivalences yieldsOne-consistency implies ${\Sigma }_1$ soundness under bounded completeness. Hence $S+{\mathrm{Con}}_S$ is consistent: if not, $S$ would prove $\neg {\mathrm{Con}}_S$, a false ${\Sigma }_1$ sentence. But in that consistent extension the last equivalence and its consistency axiom prove its own consistency ${\mathrm{Con}}_{S+{\mathrm{Con}}_S}$. Gödel's second incompleteness theorem rules this out. ThereforeThis establishes the requested unprovability using the explicit formal hypotheses, without inferring internal provability from the semantic equivalence discussed in the preceding part. The hypotheses for the second theorem are the standard effective arithmetic presentation and adequate provability predicates stipulated here.

The fixed point of boxed negated provability gives, in fact, that GL proves $F\leftrightarrow \square \perp$. Here is a direct derivation. Since $F$ is provably equivalent to a boxed formula, positive introspection and necessitation of that equivalence give $F\to \square F$. Another introspection step gives $F\to \square \square F$. The stipulated fixed point also gives $F\to \square \neg \square F$. Combining these two boxed contradictories yields $F\to \square \perp$. Conversely $\square \perp \to \square \neg \square F$ follows by normal boxed explosion, and the fixed point then yields $\square \perp \to F$.

Arithmetical soundness of GL, proved by translating distribution into the second derivability condition, necessitation into the first, and Löb's axiom into its internal arithmetic theorem, now givesAny remaining propositional parameters may be assigned arbitrary arithmetic sentences; this equivalence is uniform in those assignments. If PA is one-consistent, it is consistent and ${\Sigma }_1$ sound. Its standard provability predicate for a contradiction is then a false ${\Sigma }_1$ sentence and cannot be a theorem. Hence $F^{\ast }$ is not provable in PA. Moreover its negation is equivalent to PA's consistency statement and is unprovable by the second incompleteness theorem. Thus this fixed point is, under the stated hypothesis, undecidable rather than an unboxed reflection principle.

By part (c), one-consistency gives Sigma-1 soundness and hence ordinary consistency. First, $S$ cannot prove $\neg G$: if it did, the diagonal equivalence would give $S⊢\square G$. This is a ${\Sigma }_1$ sentence, so soundness would make it true. The stipulated standard interpretation of the arithmetical provability predicate would then supply an actual proof of $G$, contradicting consistency.

Now suppose $S⊢\square \neg G$. This too is a ${\Sigma }_1$ theorem. Soundness and the standard correctness of the predicate would imply that there is an actual $S$-proof of $\neg G$, which was just excluded. ThereforeThe two applications of soundness concern the provability assertions, not the truth of arbitrary arithmetic sentences.

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.