Use the preceding fixed point with $q=\perp$. If the chosen arithmetic interpretation sends $\perp$ to a PA-refutable sentence $Z$, it gives the arithmetic sentenceThis follows from Arithmetical soundness of GL. Since Peano arithmetic proves $\neg Z$, the two implications are equivalent to negated provability:Thus $C$ expresses the formal consistency statement for Peano arithmetic and is also a negative provability fixed point, like its Gödel sentence $G$.

Apply the supplied modal uniqueness formula to the context with a modalized occurrence $X(p)=(\square p\to \perp )$, with two fresh variables interpreted as $G$ and $C$. A modalized occurrence means that each indicated variable occurrence lies inside a box. Peano arithmetic proves both arithmetic fixed-point equations. The first derivability condition boxes those equations, so the translated uniqueness formula givesOne must not infer $G\leftrightarrow C$ by reflection. Instead, distribution and the provability of the two propositional projections give $\mathrm{PA}⊢BG\leftrightarrow BC$. Negating and using the two fixed-point equations now yieldsThis proves the Equivalence of a Gödel sentence and a consistency statement using the required modal soundness, fixed point and uniqueness results.

Take $Y(p)=p\to q$ and put $\top =(\perp \to \perp )$, $H=Y(\top )$ and $F_0=Y(\square H)=\square H\to q$. The first supplied substitution identity readsUse the supplied replacement of equivalents in the context $D(p)=p\to q$. It givesBut $H=(\top \to q)$ is equivalent to $q$. Replacement under a box gives $\square H\leftrightarrow \square q$, so $F_0$ is equivalent toReplacing equivalents once more transfers the fixed-point equation to $F$, proving $\mathrm{GL}⊢F\leftrightarrow (\square F\to q)$.

A direct check of this GL fixed point for a provability implication is useful: the Löb axiom gives $\square F\to \square q$, and necessitating the tautology $q\to F$ gives $\square q\to \square F$ by $\mathrm{K}$. Thus $\square F\leftrightarrow \square q$, and replacing the antecedent in $\square F\to q$ recovers $F$.

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 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.

Put $T=S+\{X\}$ and choose its Gödel sentence $Z$, so $T⊢Z\leftrightarrow \neg B_{T}Z$. The assumed reflection scheme gives the particular theoremThe given extension-provability implication is $S⊢B_{T}Z\to B_S(X\to Z)$. The fixed-point equivalence gives $T⊢\neg Z\to B_{T}Z$, so these implications compose toThe supplied propositional tautology $((\neg Z\to (X\to Z))\to (X\to Z))$ gives $T⊢X\to Z$, and $T⊢X$ then yields $T⊢Z$. The first of the derivability conditions for $T$ gives $T⊢B_{T}Z$, while its Gödel equivalence gives $T⊢\neg B_{T}Z$. Hence $T$ is inconsistent. By the deduction theorem for propositional logic,This proof uses diagonalization and proof transfer for the extension, and invokes neither Löb's theorem nor the second incompleteness theorem.

Use just the assumed local reflection instance with $Y=\neg X$:By the deduction theorem for propositional logic, $S⊢X\to (B_S(\neg X)\to \neg X)$. Classical propositional logic makes this imply the unconditional reflection statement $S⊢B_S(\neg X)\to \neg X$: if $X$ is false the consequent is already true, and if $X$ is true the displayed implication supplies it. Löb's theorem applied to $\neg X$ now givesThus full local reflection in a one-sentence extension is inconsistent; in this argument even the single instance concerning $\neg X$ suffices.

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.

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.

The preceding Gödel sentence argument gives $S⊢G\to {\mathrm{Con}}_S$. The permitted arithmetized positive half of the Rosser sentence argument isPure first-order logic gives $\neg BR\to R$: if there is no proof of $R$, each antecedent in its defining universal implication is false. ThereforeThis uses the supplied internal Rosser implication, rather than replacing an external nonprovability fact by an unproved internal first-order sentence.

If $S$ is inconsistent, it proves $\neg R$ by explosion. Conversely, suppose $S$ is consistent and, towards a contradiction, has a proof of $\neg R$ with standard code $n$. Consistency excludes any proof of $R$. In particular, for each $k\le n$, the closed bounded statement $\neg \mathrm{Prov}(┌R┐,\overline{k})$ is true and is provable in $S$ by Sigma-1 completeness. The true bounded statement $\mathrm{Prov}(┌\neg R┐,\overline{n})$ is also provable.

Using the given finite-numeral exhaustion below $\overline{n}$, these finitely many nonproof facts giveFor arbitrary $y$, the given comparison splits into $y\le \overline{n}$ or $\overline{n}\le y$. In the first case the antecedent $\mathrm{Prov}(┌R┐,y)$ is false. In the second case the known negative proof at code $\overline{n}$ supplies the required witness $z\le y$. Hence $S$ provesThe Rosser sentence equivalence now gives $S⊢R$, contradicting consistency. ThusOnly a fixed finite list of closed bounded facts was used; no assumption that the first-order theory is omega-consistent is needed.

Write $BA=\exists y\mathrm{Prov}(┌A┐,y)$ and fix a refutable first-order sentence $\perp$, so $S⊢\neg \perp$ and ${\mathrm{Con}}_S=\neg B\perp$. First prove the internal equivalenceBecause $\perp \to G$ is provable, the derivability conditions give $B\perp \to BG$. The fixed-point equivalence $G\leftrightarrow \neg BG$ therefore yields $G\to \neg B\perp$.

For the reverse implication, necessitating $G\to \neg BG$ and applying distribution gives $BG\to B(\neg BG)$. positive introspection gives $BG\to B(BG)$. Finally the provable implication $BG\to (\neg BG\to \perp )$, necessitated and distributed, givesConsequently $S⊢BG\to B\perp$, so $\neg B\perp \to \neg BG\to G$. The same argument works with any chosen refutable first-order sentence in place of $\perp$; their formal consistency statements are provably equivalent.

By the classical deduction theorem for propositional logic applied to adjoining a first-order sentence, $S+\{G\}$ is consistent exactly when $S⊬\neg G$. The displayed equivalence makes $S+\{G\}$ and $S+\{{\mathrm{Con}}_S\}$ deductively equivalent. ThereforeNo soundness assumption on that extension is being substituted for consistency.

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.

Given $f$, choose the hyperplane divisors as in (a). The ratios $f_Q$ form a linear subspace of $L(D)$ by (d), and its dimension equals $md+1-g=\ell (D)$ by (b). A linear subspace of a finite-dimensional vector space with the same dimension is the whole space. Hence $f=f_Q$ for some homogeneous polynomial $Q$ of degree $m$, givingThe zero function corresponds to $Q=0$. Thus every allowed meromorphic function is a ratio of homogeneous polynomials of equal degree, with a denominator that can be chosen as a product of linear forms.

Write $L_i=a_{i}x+b_{i}y+c_{i}z$ and $S={\prod }_i{L}_i$. The numerator and denominator have the same homogeneous degree, so their ratio is well-defined on projective points away from its poles and extends as a meromorphic function on $C$. Locally the pole order cannot exceed the zero order of $S{|}_C$, whose divisor is $D$. Thus $f_Q\in L(D)$.

Equality of two ratios is equivalent to $Q-Q^{\prime }$ vanishing on $C$. A nonsingular projective plane curve is irreducible: distinct positive-degree components would intersect by Bézout's theorem, producing a singular point. Its homogeneous vanishing ideal is therefore generated by its irreducible defining polynomial $P$. One can also see this using Bézout's theorem: a homogeneous polynomial not divisible by $P$ has only finitely many intersections with $C$, so cannot vanish on the whole curve. ConsequentlyMultiplication by the nonzero polynomial $P$ is injective. The linear map $V_m\to L(D)$ therefore has kernel $P{V}_{m-d}$ and image dimensionThe assumption $m\ge d$ makes both polynomial-space dimensions applicable directly.