Let $F_n$ be the formulas whose free variables are among $x_1,\dots ,x_n$. Define $\varphi E_n(T)\psi$ when $T\models \forall \bar{x}(\varphi \leftrightarrow \psi )$. The n-variable Lindenbaum algebra quotient is a Boolean algebra, with meet, join and complement induced by conjunction, disjunction and negation; its zero and one are contradiction and truth classes. Its order is $[\varphi ]\le [\psi ]$ exactly when $T\models \forall \bar{x}(\varphi \to \psi )$.

The Ryll-Nardzewski theorem states that for a complete theory with infinite models in a countable language, the following are equivalent: the theory is countably categorical; for every finite $n$ there are only finitely many complete $n$-types over the empty set; and every Boolean algebra $F_n/E_n(T)$ is finite. Equivalently each such type is isolated. The countable-language and completeness hypotheses are essential parts of this formulation.

A theory is $\kappa$-categorical if it has a model of cardinality $\kappa$ and any two models of that cardinality are isomorphic. The existence clause prevents vacuous categoricity at cardinalities where there is no model.

To show that infinite-cardinal categoricity forces completeness, suppose $T$ were incomplete. Then some sentence $\sigma$ has both $T+\sigma$ and $T+\neg \sigma$ satisfiable, by completeness of first-order logic. Their models must be infinite because $T$ has no finite models. For an infinite $\kappa \ge |L|$, the upward and downward Löwenheim-Skolem theorems produce a model of each extension of cardinality exactly $\kappa$: pass to an elementary submodel of size at most $\max (|L|,{\aleph }_0)$ and then to the desired size, or reduce a larger model to that size. Categoricity makes these two models isomorphic, but one satisfies $\sigma$ and the other its negation. Contradiction. Therefore $T$ is complete. If language size is defined without automatically including ${\aleph }_0$, the infinite-cardinal qualification is explicit; the assumed existence of a $\kappa$-sized model and absence of finite models already force it here.

Existential sentences are preserved under extensions: witnesses remain present and quantifier-free truth is unchanged by an embedding. Therefore any existential axiomatization implies the specified extension-closure property.

For existential axiomatization from extension closure, let $E$ be all existential consequences of $T$, and suppose $A\models E$. We claim that $T\cup {\mathrm{Th}}_{\forall }(A)$ is satisfiable. Otherwise compactness supplies finitely many universal sentences ${\theta }_1,\dots ,{\theta }_m$ true in $A$ such that $T\models \neg ({\theta }_1\wedge \cdots \wedge {\theta }_m)$. The finite conjunction is universal after renaming bound variables, so its negation is existential. It belongs to $E$ but is false in $A$, a contradiction.

The preceding universal-theory embedding result now yields $B\models T$ and $A^{\ast }\equiv A$ with $B\subseteq A^{\ast }$. By the assumed extension closure, $A^{\ast }\models T$; elementary equivalence implies $A\models T$. Thus $E$ axiomatizes exactly the models of $T$, proving existential axiomatizability is equivalent to closure under extensions. This includes the inconsistent case, whose empty model class is axiomatized by an existential contradiction.

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.

GL has all classical propositional tautologies, the normal distribution axiom $\square (A\to B)\to (\square A\to \square B)$ and the Löb axiom $\square (\square A\to A)\to \square A$, closed under uniform substitution, modus ponens and necessitation of theorems. We use its derived positive-introspection theorem $\square A\to \square \square A$, normal boxed reasoning, and the boxed replacement principle supplied in the question.

For completeness, positive introspection follows from these axioms. Put $C=A\wedge \square A$. Distribution gives $\square C\to \square A$, so propositional logic proves $A\to (\square C\to C)$. Necessitate and distribute to get $\square A\to \square (\square C\to C)$; Löb's axiom gives $\square A\to \square C$, and boxing $C\to \square A$ finishes $\square A\to \square \square A$.

For a GL fixed point by truth substitution, set $\top =(\perp \to \perp )$, $U=\square Y(\top )$ and $V=\square Y(U)$. From the tautology $U\to (\top \leftrightarrow U)$, boxed reasoning gives $\square U\to \square (\top \leftrightarrow U)$. The supplied replacement principle and distribution then giveSince $U$ is itself boxed, positive introspection gives $U\to \square U$, and hence $U\to V$.

For the reverse direction, the displayed implication entails the theorem $V\to (\square U\to U)$. Necessitate it and distribute to obtain $\square V\to \square (\square U\to U)$. Since $V$ is boxed, $V\to \square V$ holds. The Löb axiom therefore yields $V\to \square U$, and the same displayed implication then yields $V\to U$. ConsequentlyAll occurrences of the unknown letter have been removed from $U$ by substitution of truth; any other parameter letters remain available. The proof does not assume the invalid reflection principle $\square U\to U$ as an unconditional axiom.

Suppose $S+A$ proves every specified reflection instance. Use only the instance with $X=\neg A$. The deduction theorem givesClassical propositional reasoning turns this into $S⊢\square \neg A\to \neg A$: if $\neg A$ already holds the implication is true, while otherwise $A$ holds and the displayed theorem supplies it. Löb's theorem now yields $S⊢\neg A$, making $S+A$ inconsistent. Therefore no sentence consistent with $S$ can supply all the local reflection instances in a one-sentence extension. The proof uses just one well-chosen instance, and never applies necessitation to a derivation with the extra assumption still open.

Gödel's second incompleteness theorem says that a consistent effectively presented arithmetic theory with an adequate proof predicate cannot prove its formal consistency statement. The background strength must support the diagonal lemma and the derivability conditions, as in the present arithmetic setting.

Löb's theorem saysIt is a theorem about derivability for every sentence $A$, not merely an external soundness assertion about the interpretation of $\square$. Taking $A=\perp$, a proof of consistency gives $S⊢\square \perp \to \perp$; Löb then gives $S⊢\perp$. Thus a consistent $S$ cannot prove consistency. This is how the second incompleteness theorem is the contradiction-sentence instance of Löb's more general result.

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.