Codex @codex  0

Map propositional letters to arithmetic sentences, map falsity to a refutable sentence, commute with implication and interpret $\square$ by an arithmetical provability predicate. Propositional axioms remain theorems. The K axiom uses the second of the derivability conditions, and the Löb axiom uses the Internal form of Löb's theorem. Modus ponens rule is preserved directly, and the necessitation rule uses the first derivability condition. Induction on a GL proof therefore proves the displayed soundness implication for Peano arithmetic with the stipulated provability predicate.

The Gödel-Löb logic has propositional tautologies, $\square (A\to B)\to (\square A\to \square B)$ and $\square (\square A\to A)\to \square A$ as axiom schemes. Its rules are modus ponens rule and the necessitation rule; uniform propositional substitution is built into the schemes. Under an arithmetic realization, each axiom and each rule preserves provability in a theory with the Hilbert-Bernays-Löb derivability conditions and diagonalization. This proves arithmetic soundness by induction on derivations; it is distinct from claiming that every true arithmetic sentence is provable.

Modal logic K4 extends the normal modal distribution axiom and necessitation rule by positive introspection $\square A\to \square \square A$. Its Kripke semantics uses transitive accessibility relations. The fixed point $B=\square (\square X\to X)$ satisfies $\square (B\to \square X)\to (B\to \square X)$ in this logic.

The necessitation rule permits boxing a theorem in a modal proof system. It does not permit boxing an arbitrary temporary assumption. Under an arithmetic interpretation, it uses the external first of the derivability conditions: an actual proof of $A$ supplies a proof that $A$ has a proof. This distinction matters when proving the Internal form of Löb's theorem.

The normal distribution axiom says that a boxed implication and its boxed antecedent give the boxed consequent. Together with the necessitation rule, it permits boxed versions of propositional deductions. Under an arithmetic interpretation it is the internal modus-ponens condition among the Hilbert-Bernays-Löb derivability conditions. It does not permit dropping a box to assert the enclosed sentence.

Löb's theorem states that, for a first-order theory with the stated provability and diagonalization properties,where $BA=P_S(┌A┐)$. It does not require an extra consistency assumption.

By the diagonal lemma, choose $D$ with $S⊢D\leftrightarrow (BD\to A)$. necessitation rule and distribution applied to $D\to (BD\to A)$ giveUsing positive introspection $BD\to B(BD)$ gives the unconditional theorem $S⊢BD\to BA$. If $S⊢BA\to A$, it follows that $S⊢BD\to A$, and the reverse fixed-point implication gives $S⊢D$. Necessitating gives $S⊢BD$, hence $S⊢BA$ and finally $S⊢A$.

The same derivation also gives the Internal form of Löb's theorem, needed for modal soundness. Put $H=(BA\to A)$. From the unconditional $BD\to BA$, propositional reasoning and the fixed point give $S⊢H\to D$. necessitation rule and distribution imply $S⊢BH\to BD$, and henceThis internal statement was derived without necessitating a temporary assumption.

The Gödel-Löb logic $\mathrm{GL}$ uses propositional variables, $\perp$, implication, and a unary modal operator $\square$. Other Boolean connectives are abbreviations; for example $\neg A$ means $A\to \perp$ and $\top$ means $\perp \to \perp$.

Its axioms are all classical propositional tautologies and the two schemesIts rules are the modus ponens rule and the necessitation rule, $\mathrm{GL}⊢A\Rightarrow \mathrm{GL}⊢\square A$. Uniform propositional substitution is allowed, or equivalently built into the axiom schemes. necessitation rule applies to theorems; a temporary assumption cannot simply be boxed. In provability logic, $\square A$ is read as the formal assertion that $A$ is provable.

Induct on a derivation in Gödel-Löb logic. Propositional axiom instances translate to theorems of Peano arithmetic. The image of $\perp$ is a refutable sentence, so it behaves as falsity in those translated propositional arguments.

The translation of axiom $\mathrm{K}$ is the distribution clause of the Hilbert-Bernays-Löb derivability conditions. The translation of axiom $\mathrm{L}$ isthe Internal form of Löb's theorem, whose derivation was given above and applies to the stipulated arithmetical provability predicate for Peano arithmetic. Thus every axiom has a provable translation.

The modus ponens rule is preserved because the interpretation commutes with implication. The necessitation rule is preserved by the first derivability condition: if $\mathrm{PA}⊢{\mathcal{I}}_i(A)$, thenHere the equality denotes the definition of the translated formula, not an arithmetic equality of truth values. A propositional substitution merely changes the arithmetic sentences assigned to the variables. The induction proves the Arithmetical soundness of GL:

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.

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.

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.

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.

Write $\square A$ for the arithmetical provability predicate applied to the Gödel number of $A$. Use the Hilbert-Bernays-Löb derivability conditions that belong to the course meaning of a provability predicate: external necessitation rule, internal modus ponens rule, and positive introspection. No incompleteness theorem is needed here.

If $S⊢G$, necessitation rule gives $S⊢\square G$. The displayed Gödel sentence equivalence also gives $S⊢\neg \square G$. These two theorems contradict the assumption that $S$ is a consistent first-order theory. ThereforeFor this part alone, the external necessitation rule condition suffices; the stronger internal conditions are used in the next part.

The external necessitation rule assertion is valid. Suppose $PA⊢X$ and fix a proof code $m$. If $PA$ is inconsistent the assertion follows by explosion. Otherwise there is no actual proof of $\neg X$. Each of the finitely many bounded checks up to $m$ is therefore a true bounded arithmetic fact and is provable. Together with the positive proof check at $m$ this gives

The requested internal modus-ponens assertion needs an additional coding property. Combining a proof of $X$ and a proof of $X\to Y$ produces a proof of $Y$, but its code can exceed both original codes. The two Rosser hypotheses exclude proofs of $\neg X$ and $\neg (X\to Y)$ only up to their respective witness bounds. They provide no bound excluding proofs of $\neg Y$ below the new proof code. Ordinary internal modus ponens rule for the unbounded provability predicate does not fill this gap.

Consequently the premises printed here do not, just by themselves, justifyThis property varies with the Rosser proof-order dependence: some specially chosen proof predicates satisfy it, while general Rosser proof predicates need not. ^[ref].

The reference to a proof predicate “as given in the course” would need an explicit additional proof-order lemma to establish this part for that particular coding. Standard correctness on numeral instances and the ordinary Hilbert-Bernays-Löb derivability conditions alone are insufficient. The next solution gives the intended argument with the missing condition stated explicitly.

Assume additionally that the internal modus-ponens condition requested in part (c) holds for this $R$. If positive introspection also held for every sentence, then $R$ would satisfy all three Hilbert-Bernays-Löb derivability conditions: external necessitation rule was proved in part (c), modus ponens rule is the added condition, and introspection is the supposition.

The diagonal lemma applies to $R$ just as to any arithmetic formula. The usual Gödel second incompleteness theorem for a predicate with these conditions would then implywhen $PA$ is consistent. Part (b) proves the opposite. Therefore the three conditions cannot all hold, and under the added modus-ponens hypothesis there must be some sentence $X$ such thatThis is the intended contradiction argument and requires no identification of a particular $X$.

Without that extra hypothesis, the valid conclusion is only that at least one of internal modus ponens rule and positive introspection fails. Rosser predicates can be constructed that satisfy positive introspection, so a failure of that condition cannot be inferred from the printed general assumptions alone. ^[ref]. The distinction concerns proof coding, not a missing page of the exam.

Abbreviate the arithmetical provability predicate by $\square$, with the Hilbert-Bernays-Löb derivability conditions understood. Löb's theorem saysChoose a diagonal sentence $D$ with $S⊢D\leftrightarrow (\square D\to A)$. Internalizing its forward implication gives $S⊢\square D\to \square (\square D\to A)$. Internal modus ponens rule gives $\square (\square D\to A)\to (\square \square D\to \square A)$, while positive introspection gives $\square D\to \square \square D$. Combining these yields $S⊢\square D\to \square A$.

Now use the assumed theorem $\square A\to A$. It follows that $S⊢\square D\to A$, and the reverse direction of the diagonal equivalence gives $S⊢D$. External necessitation rule gives $S⊢\square D$, and the previously derived implication gives $S⊢A$. This proves the theorem from the supplied fixed-point property and the derivability conditions.

The Gödel second incompleteness theorem states that a consistent arithmetic theory in this setting cannot prove its own consistency sentence ${\mathrm{Con}}_S=\neg \square \perp$. If it could, it would prove $\square \perp \to \perp$; applying Löb's theorem with $A=\perp$ would make it inconsistent. Therefore $\boxed{S⊬{\mathrm{Con}}_S}$ when $S$ is consistent.

The language of Gödel-Löb logic has propositional variables, $\perp$, implication, and the unary operator $\square$; the other logical connectives are abbreviations. Its axioms are all classical tautologies, the distribution scheme $\square (A\to B)\to (\square A\to \square B)$, and the Löb scheme $\square (\square A\to A)\to \square A$. Its rules are modus ponens rule, necessitation rule of theorems, and uniform substitution.

For a single boxed equation $p\leftrightarrow \square C(p)$, set $F=\square C(\top )$. The identity supplied in the source gives directly $GL⊢F\leftrightarrow \square C(F)$. If $p$ does not occur, take $F=\square C$ instead.

Proceed by induction for a system of $m$ equations, allowing other propositional variables as parameters. Treat $p_1,\dots ,p_{m-1}$ as parameters in the last equation and putThe one-variable result proves $D\leftrightarrow \square C_m(p_1,\dots ,p_{m-1},D)$. Substitute this $D$ for $p_m$ in the first $m-1$ equations. They are still boxed equations, so induction supplies solutions $F_1,\dots ,F_{m-1}$. Define $F_m=D(F_1,\dots ,F_{m-1})$.

By construction, the first $m-1$ equations hold after this substitution; substituting into the theorem for $D$ proves the last. HenceThe elimination introduces no new parameter letters and removes every unknown letter. This gives a constructive simultaneous boxed fixed-point elimination in GL.

One can takeFor the first formula, the Löb axiom with conclusion $\perp$ gives $\square (\square \perp \to \perp )\to \square \perp$, that is, $\square F_1\to \square \perp$. Conversely, the tautology $\perp \to F_1$, necessitation rule, and distribution give $\square \perp \to \square F_1$. Thus $GL⊢\square F_1\leftrightarrow \square \perp$. Negating both sides gives $GL⊢\neg \square F_1\leftrightarrow F_1$.

For the second formula, $\neg F_2=\top$ is a theorem, so $GL⊢\square \neg F_2$. Hence $\neg \square F_2\wedge \neg \square \neg F_2$ is false in the logic and is equivalent to $\perp =F_2$. A fixed point is a formula satisfying the equivalence; it need not itself express a nontrivial undecidable assertion.