Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2008 / A / 3

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

Put $T=S\cup \{\neg X\}$ and assume $S⊢P_S(┌X┐)\to X$. In $T$, contraposition against its extra axiom gives $\neg P_S(┌X┐)$.

Classical logic proves $(\neg X\to X)\to X$. By the derivability conditions,Compose this with the supplied formalized deduction implication from $P_T(┌X┐)$ to its left-hand side. Then $T$ provesand thereforeThe other supplied assumption says this is impossible if $T$ is first-order consistent. Thus $T$ is inconsistent. By the deduction theorem, inconsistency after adjoining $\neg X$ yields $S⊢\neg \neg X$, henceThis establishes Löb's inference rule using precisely the strengthened unprovability assumption and the formalized deduction property supplied in the question.

Take a first-order sentence $Y$ refutable in $S$ and suppose, toward contradiction, that a first-order consistent $S$ proved $\neg P_S(┌Y┐)$. Propositional logic would then giveLöb's inference, applied with $X=Y$, would give $S⊢Y$, contradicting the existing formal proof of $\neg Y$. Hence first-order consistency excludes the proposed formal proof of non-provability.

Thus the familiar unprovability of the first-order consistency statement associated with a refutable first-order sentence is a special consequence of the general ruleThe general rule applies to every first-order sentence, not just a chosen false or refutable one.

Let $j=i+n$ with $n\ge 1$. Positive introspection supplies the theorem $F_k\to F_{k+1}$ for every $k\ge 1$, since $F_k$ itself has the form $P_S(┌F_{k-1}┐)$.

Induction on $n$ consequently givesAt $n=1$ this is the identity implication. To pass from $n$ to $n+1$, compose the induction hypothesis with the positive-introspection implication at $k=i+n$, which is at least one. Composing the result with the assumed $F_j\to F_i$ givesi.e. $S⊢P_S(┌F_i┐)\to F_i$. Löb's rule now yieldsThe index restriction on positive introspection has been respected even when $i=0$: the chain begins at $F_{i+1}$, which already is a provability assertion.