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

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.

Abbreviate $P(┌A┐)$ by $\square A$. Since $S⊢\neg X$, it proves $X\to G$. The theoremhood and distribution conditions giveThe fixed-point equation gives $S⊢G\to (\square G\to X)$, because $G$ implies $\neg \square G$ and a false antecedent implies any conclusion. Applying theoremhood and distribution yieldsPositive introspection gives $\square G\to \square \square G$; distribution then gives $\square G\to \square X$. Thus $S⊢\square G\leftrightarrow \square X$. Combining with $G\leftrightarrow \neg \square G$ provesIn particular, choosing a fixed logical contradiction for $X$ identifies this Gödel sentence with the formal consistency statement of $S$.

If $S⊢G$, theoremhood gives $S⊢\square G$, while the fixed-point equivalence also gives $S⊢\neg \square G$. Therefore first-order consistency implies $S⊬G$.

If $S\cup \{\neg G\}$ were inconsistent, the deduction theorem and classical propositional logic would give $S⊢\neg \neg G$, hence $S⊢G$. This is impossible by the preceding argument. ThereforeThis is a syntactic first-order consistency result. It does not claim that the extra axiom is true in the standard natural numbers or that the extended first-order theory is sound.

First establish the transfer of provability requested in the hint. The propositional theorem $X\to (\neg G\to X)$ and the derivability conditions giveThe supplied arithmetized deduction equivalence identifies the right-hand provability assertion, within $S^{\ast }$, with ${\square }^{\ast }X$. HenceChoose a fixed contradiction $\perp$ for $X$. Part (b) gives $S⊢G\leftrightarrow \neg \square \perp$, so adjoining $\neg G$ gives $S^{\ast }⊢\square \perp$. The transfer implication now gives $S^{\ast }⊢{\square }^{\ast }\perp$.

Apply (b) inside $S^{\ast }$ to its own Gödel sentence: it proves $G^{\ast }\leftrightarrow \neg {\square }^{\ast }\perp$. The last provability assertion therefore entailsThus the extension proves the negation of its own Gödel sentence as well. When $S$ is first-order consistent, (c) says this phenomenon occurs in a first-order consistent extension; the extension asserts an internal formal proof of contradiction without there being an actual standard formal proof of contradiction.