The literal semantic hypothesis is insufficient: a semantic Gödel fixed point need not be canonical. A sentence can be false and provable in a consistent, unsound arithmetic theory, in which case both sides of the stipulated semantic biconditional can be false.

For a concrete counterexample, assume PA is consistent and set $S=\mathrm{PA}+\neg {\mathrm{Con}}_{\mathrm{PA}}$. Gödel's second incompleteness theorem makes this extension consistent: otherwise PA would prove its own consistency. It is still bounded-complete. Use ordinary numeralwise proof and refutation enumerators for this recursively axiomatized theory, and take $G=\neg {\mathrm{Con}}_{\mathrm{PA}}$. This $G$ is false in the standard natural numbers but is an axiom of $S$. Since it is provable, $\exists yP(┌G┐,y)$ is true; its negation is false. Thus the semantic fixed-point biconditional required in this part is true, with both sides false.

Choose $R$ by the usual canonical Rosser construction for these proof matrices. Its undecidability follows from the preceding parts, and it is a true ${\Pi }_1$ sentence: if it were false, its true ${\Sigma }_1$ negation would be provable in this bounded-complete theory, contradicting undecidability. Hence $G$ is false and $R$ true, so their proposed semantic equivalence is false. This counterexample meets the literal assumptions and does not exploit a missing source page.

Under the intended canonical ${\Pi }_1$ Gödel/Rosser convention, the expected answer does hold. Consistency plus bounded completeness implies ${\Pi }_1$ soundness: a false ${\Pi }_1$ theorem has a standard bounded counterexample whose negation the theory proves. If canonical $G$ were false, its truth fixed point would make it provable, contradicting this soundness; thus $G$ is true. Canonical $R$ is true by the preceding ${\Sigma }_1$-negation argument, so both canonical sentences are true and their equivalence is true. This last conclusion needs that canonical construction or an equivalent additional restriction; truth of a biconditional alone does not supply it.

For Rosser separation by a bounded stage comparison, use the numeralwise enumeration in arithmetic properties meant by enumeration in $S$: membership supplies some standard stage with a provable positive instance, while nonmembership makes every standard-stage instance refutable. These are stronger than merely attaching a ${\Sigma }_1$ syntactic label to an arbitrary formula. The finite-initial-segment axiom lets us combine finitely many numeralwise refutations into a bounded universal assertion.

If $n$ is provable, choose a standard stage $p$ with $S⊢P(\overline{n},\overline{p})$. Consistency means $n$ is not refutable. Therefore $S⊢\neg R(\overline{n},\overline{j})$ for each $j\le p$. Using the displayed finite-segment axiom and equality substitution, combine these proofs to get $S⊢\forall z\le \overline{p}\neg R(\overline{n},z)$. Existential introduction with stage $p$ proves the separator at $n$.

If $n$ is refutable, choose a standard stage $q$ with $S⊢R(\overline{n},\overline{q})$. Consistency implies that $n$ is not provable, so all standard instances of $P(\overline{n},\cdot )$ are refutable. In particular their finitely many instances through $q$ give $S⊢\forall z\le \overline{q}\neg P(\overline{n},z)$. For an arbitrary proposed witness $z$, the total-comparison axiom gives $z\le \overline{q}$ or $\overline{q}\le z$. In the first case its $P$ conjunct fails; in the second case the known $R$ instance at $q$ contradicts its bounded no-refutation conjunct. Generalize on $z$ to refute the existential separator. Hence the proposed first-proof-before-refutation formula separates the two sets.

For separation of number sets in an arithmetic theory, a formula separates $A$ from $B$ in $S$ if $n\in A$ implies $S⊢F(\overline{n})$, and $n\in B$ implies $S⊢\neg F(\overline{n})$. No demand is made for numbers outside their union. Consistency forces disjointness when such a separator exists.

Let $r$ be the code of the fixed-point sentence. If $S⊢R$, then $r$ is in the provable set, so separation gives $S⊢H(\overline{r})$. The fixed-point equivalence gives its negation, a contradiction. If $S⊢\neg R$, then $r$ is in the refutable set, so separation gives $S⊢\neg H(\overline{r})$, and the fixed-point equivalence gives $S⊢R$, again a contradiction. ThusThe argument is syntactic: it needs only the separating implications and consistency, not omega-consistency or general soundness.

For unrestricted consistency self-strengthening is inconsistent, again take $A=S+\neg {\mathrm{Con}}_S$. In $S^{++}$ the axiom ${\mathrm{Con}}_S$ and the preceding implication prove ${\mathrm{Con}}_A$. The additional rule then proves ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$.

However consistency of an extension implies consistency of its subtheory by the formalized inclusion of proofs: $S⊢{\mathrm{Con}}_A\to {\mathrm{Con}}_S$. Thus the ordinary theory $A+{\mathrm{Con}}_A$ contains $\neg {\mathrm{Con}}_S$ and derives ${\mathrm{Con}}_S$, so it has a finite contradiction proof. Checking that concrete proof in arithmetic gives $S⊢\neg {\mathrm{Con}}_{A+{\mathrm{Con}}_A}$. This theorem is also present in $S^{++}$, contradicting the result of the new rule. Therefore $S^{++}$ is inconsistent.

The error in the added rule is its unrestricted internal use on arbitrary arithmetically presented systems, including systems containing false consistency assertions. A true external consistency progression for a specified sound system is not this unrestricted inference rule.

For consistency of a negated-consistency extension, put $A=S+\neg {\mathrm{Con}}_S$. The arithmetized deduction theorem, together with double-negation elimination and formalized proof transformations, givesFrom the preceding proof, $S⊢{\square }_{S}G\to {\square }_S\perp$. Necessitating the equivalence between $G$ and ${\mathrm{Con}}_S$ and using distribution therefore gives $S⊢{\square }_S{\mathrm{Con}}_S\to {\square }_S\perp$. Its contrapositive isThis is an internal conditional statement. It does not assert that $S$ proves its own consistency or permits the consistency premise to be discarded.

The Hilbert-Bernays-Löb derivability conditions are: if $S⊢A$ then $S⊢\square A$; $S⊢\square (A\to B)\to (\square A\to \square B)$; and $S⊢\square A\to \square \square A$. The first is an external rule about provability; the latter two are internal theorems. Standard numerical correctness and the stipulated ${\Sigma }_1$ form accompany the predicate in this question. These conditions do not include reflection $\square A\to A$.

Choose a fixed refutable sentence $\perp$ and identify ${\mathrm{Con}}_S$ with $\neg \square \perp$. Different fixed refutable choices have provably equivalent consistency sentences, because $S$ proves their equivalence to a contradiction. From $\perp \to G$, necessitation and distribution give $\square \perp \to \square G$. Since $G\to \neg \square G$, this yields $G\to {\mathrm{Con}}_S$.

For the converse, necessitate $G\to \neg \square G$ and distribute to get $\square G\to \square \neg \square G$. Positive introspection also gives $\square G\to \square \square G$. The two boxed contradictories imply $\square \perp$ by formalized propositional reasoning. Thus $\square G\to \square \perp$, and contraposition gives ${\mathrm{Con}}_S\to \neg \square G\to G$. ConsequentlyFinally the deduction theorem says that $S+G$ is inconsistent exactly when $S⊢\neg G$. The internal equivalence identifies $S+G$ and $S+{\mathrm{Con}}_S$ in their deductive consequences. Hence $S⊬\neg G$ exactly when $S+{\mathrm{Con}}_S$ is consistent. Consistency of $S$ alone need not ensure this stronger consistency condition.

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.

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.

Enumerate the standard positive primes as $(p_n{)}_{n<\omega }$. For each subset $A\subseteq \omega$ consider the partial typewhere divisibility is the ring logical formula $\exists y({\bar{p}}_{n}y=x)$.

Every finite subset is realized in $\mathbb{Z}$: take the product of the finitely many primes required to divide $x$, or $1$ if there are none. This is nonzero and is not divisible by any of the distinct finitely many primes required not to divide it. Compactness theorem supplies a complete type extending $q_A$.

Distinct subsets $A,B$ yield distinct complete extensions, because at an index in their symmetric difference they require opposite divisibility statements. There are $2^{{\aleph }_0}$ such subsets, so there are at least that many complete one-types. There are at most that many because the first-order language has only countably many logical formulas and a partial type is a set of them. HenceIn particular the number of complete one-types is uncountable, despite every partial type realized in the particular countable first-order model $\mathcal{Z}$ being a principal complete type.

Take the parameter-free complete typeof the nonstandard prime constructed in part (i). It is first-order consistent and complete because it consists of exactly the logical formulas true of an actual element in a first-order model of $T$. It contains $x\ne \bar{a}$ for every integer $a$, and consequently no element of $\mathcal{Z}$ realizes it. ThusIt is necessarily a nonprincipal complete type. If a first-order consistent logical formula isolated it, completeness of $T$ would force the existential closure of that logical formula to hold in every first-order model of $T$, including $\mathcal{Z}$; a witness there would realize the partial type, a contradiction. This connects the explicit omission with the hypothesis of the omitting types theorem.

Every integer is definable without parameters in the ring first-order language. For $a\ge 0$, use $x=\bar{a}$; for $a=-m<0$, use $x+\bar{m}=0$. For a finite tuple $\vec{a}$, the conjunction ${\delta }_{\vec{a}}(\vec{x})$ of these coordinate logical formulas uniquely defines that tuple in $\mathcal{Z}$.

If $\varphi (\vec{x})$ belongs to its complete type, the first-order sentenceis true in $\mathcal{Z}$, since there is only the specified tuple to check. It therefore belongs to $T=\mathrm{Th}(\mathcal{Z})$. The logical formula ${\delta }_{\vec{a}}$ is first-order consistent with $T$, since it is realized in $\mathcal{Z}$, and implies every member of the partial type modulo $T$. Hence every complete type realized in $\mathcal{Z}$ is a principal complete type, isolated by its tuple-defining logical formula.

Apply downward Löwenheim-Skolem to the extension from part (i), keeping all standard integers and the new prime $c$. The first-order language and this prescribed subset are countable, so there is a countable elementary substructure $N$ containing them. In particular $N\equiv \mathcal{Z}$ and contains an element outside the standard copy of $\mathbb{Z}$.

No ring isomorphism $N\to \mathcal{Z}$ can exist. Such an isomorphism fixes $0$ and $1$, hence every nonnegative integer numeral. It also fixes each negative integer, which is the unique solution of $x+\bar{n}=0$ for the corresponding positive $n$. Consequently it fixes the whole standard copy. The image of $c$ would be some standard integer $a$, already the image of that same named standard element, violating injectivity.

Thus $N$ and $\mathcal{Z}$ are two nonisomorphic countably infinite first-order models of $T$, so

Prime elements are first-order definable in the ring first-order language. For instance let $\mathrm{Unit}(u)$ mean $\exists v(uv=1)$ and useIn the integer ring this defines prime elements up to the harmless choice of sign. Expand the first-order language by names for every integer and a new constant $c$. Take the elementary diagram of $\mathcal{Z}$ together withEvery finite subset is satisfiable in $\mathcal{Z}$: choose a positive prime integer outside the finitely many excluded values, using the Euclid's theorem. Compactness theorem gives a first-order model of the entire set. The complete-diagram argument embeds $\mathcal{Z}$ elementarily into its reduct; identify that copy with the original integer ring.

The resulting elementary extension contains $c$, a prime element unequal to every named standard integer. ThereforeThe construction rules out all standard integers, not merely the finite list appearing in any one approximation.

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.