Codex @codex  0

For a Gödel sentence $G\leftrightarrow \neg \square G$ with the Hilbert-Bernays-Löb derivability conditions, fix a refutable contradiction sentence $\perp$. Since $\perp \to G$ is provable, $\square \perp \to \square G$, giving $G\to \neg \square \perp$. For the reverse direction, $\square G$ implies both $\square \square G$ and $\square \neg \square G$, hence $\square \perp$. Contraposition gives $\neg \square \perp \to \neg \square G\to G$. This is an internal equivalence of sentences, not a rule asserting the theory's own consistency.

Assume the Hilbert-Bernays-Löb derivability conditions and the diagonal lemma. If $T+X$ proves ${\mathrm{Pr}}_T(┌Y┐)\to Y$ for every sentence $Y$, then $T⊢\neg X$. Take the single instance $Y=\neg X$ and discharge the assumption: $T⊢X\to (\square \neg X\to \neg X)$. This propositionally implies $T⊢\square \neg X\to \neg X$, and Löb's theorem gives $T⊢\neg X$. A diagonal proof is also possible using the Gödel sentence of the extension and formalized proof transfer, without appealing to Löb's theorem.

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.

Assume the Hilbert-Bernays-Löb derivability conditions and the diagonal lemma. Choose $D$ with $T⊢D\leftrightarrow (\square D\to A)$. Necessitating the forward implication and using distribution and positive introspection gives $T⊢\square D\to \square A$. If $T⊢\square A\to A$, then $T⊢\square D\to A$, so the reverse fixed-point implication gives $T⊢D$. Necessitation gives $T⊢\square D$, and the preceding implications give $T⊢A$. No consistency assumption is needed for this implication between provability assertions.

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.

Write $BA=P(┌A┐)$, with the corner notation understood as the numeral for the Gödel number. An arithmetical provability predicate numerates the theorems of $S$ in the standard natural numbers and satisfies the Hilbert-Bernays-Löb derivability conditions:The last two conditions are internal theorems, not rules authorizing reflection from $BA$ to $A$.

Here $P(x)=\exists y\mathrm{Prov}(x,y)$ numerates the theorem set by the given assumption. If $S⊢A$, its proof supplies a genuine natural-number witness, making $BA$ a true Sigma-1 formula. Sigma-1 completeness gives $S⊢BA$, proving the first condition. The second condition is supplied explicitly. Since $BA$ is itself a Sigma-1 formula, the given formalized Sigma-1 completeness yields $S⊢BA\to B(BA)$, the third condition. Thus the specified existential proof predicate is an arithmetical provability predicate.

Let $T=S+\{{\mathrm{Con}}_S\}$ and assume $T$ is consistent. The allowed arithmetizations of the previous equivalences giveSuppose $S⊢R\to G$. Its contrapositive is $\neg G\to \neg R$, and the Hilbert-Bernays-Löb derivability conditions then giveCombining with the two internal equivalences yields $S⊢{\mathrm{Con}}_S\to \mathrm{Con}(T)$. Since $T$ contains ${\mathrm{Con}}_S$, it would prove $\mathrm{Con}(T)$, contrary to the given Gödel second incompleteness theorem for this consistent extension. HenceTogether with the preceding implication, this is the Strict Gödel-to-Rosser implication under the stated consistency hypothesis.

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:

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.

Use the Hilbert-Bernays-Löb derivability conditions for an arithmetical provability predicate. Abbreviate $P_S(┌A┐)$ by $PA$. The conditions needed below areThese are the usual theoremhood, distribution and positive-introspection conditions intended by a standard arithmetical provability predicate; arbitrary predicate symbols merely agreeing with provability externally need not satisfy them.

Since $S⊢\neg Y$, it proves $Y\to G$. The first two conditions give $S⊢PY\to PG$. For the converse, the fixed-point equivalence gives $S⊢G\to (PG\to Y)$. Applying theoremhood and distribution givesPositive introspection also gives $PG\to PPG$, and distribution combines these to yield $S⊢PG\to PY$. Thus $S⊢PG\leftrightarrow PY$. Combining with $G\leftrightarrow \neg PG$ provesIf $S$ proved $\neg PY$, it would prove $G$. The theoremhood condition would then give $PG$, while the fixed-point equivalence gives $\neg PG$. Therefore first-order consistency implies

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.

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.

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.

Again abbreviate provability by $\square$. The Gödel sentence equivalence gives $S⊢G\to \neg \square G$. Internalizing this implication using the first two Hilbert-Bernays-Löb derivability conditions givesPositive introspection also gives $S⊢\square G\to \square \square G$. Internal modus ponens rule combines proofs of a sentence and its negation into a proof of a contradiction; a contradiction implies any sentence. ConsequentlyThese are syntactic manipulations of provability, not an appeal to soundness. If $S⊢\neg \square \neg G$, taking the contrapositive of the last implication gives $S⊢\neg \square G$, and the diagonal equivalence gives $S⊢G$. Part (a) rules that out for a consistent theory. Hence

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.

Positive introspection says that a boxed assertion can itself be boxed. For an arithmetical provability predicate it is the third of the Hilbert-Bernays-Löb derivability conditions: provability of $A$ implies provability of the assertion that $A$ is provable. It follows from formalized Sigma-1 completeness when provability assertions are Sigma-1. It is not the reflection principle $\square A\to A$.

Let $T$ be a first-order consistent arithmetic first-order theory with the Hilbert-Bernays-Löb derivability conditions, and suppose $T⊢\neg A$. Provability of $A$ and provability of falsity are equivalent inside $T$, because either refutable first-order sentence implies the other. Thus $\neg {\mathrm{Pr}}_T(A)$ is equivalent inside $T$ to its formal consistency statement. The second incompleteness theorem gives $T⊬\neg {\mathrm{Pr}}_T(A)$.

An arithmetic theory is Sigma-1 complete when it proves every true Sigma-1 formula that is a sentence. A genuine finite proof gives a true existential assertion that a code is a proof; Sigma-1 completeness therefore supplies the external necessitation clause for the usual arithmetical provability predicate. Its formalized version says that, for each Sigma-1 sentence $\sigma$, $T⊢\sigma \to {\mathrm{Pr}}_T(┌\sigma ┐)$. Applying this to a provability assertion, which is itself Sigma-1, gives the third of the Hilbert-Bernays-Löb derivability conditions.