Take $\square A={\mathrm{Pr}}_{PA}(┌A┐)$ for the standard formal proof predicate symbol and putUse as given the arithmetization of syntax in PA, the derivability conditions, and the diagonal lemma. The latter supplies the fixed point needed in (a), and the former conditions interpret its normal modal distribution, necessitation on theorems and axiom4. Thus the argument in (a) proves the internal Löb implication in PA. With $X=\perp$ it readsThe inner implication is the first-order consistency first-order sentence $\neg \square \perp$, so contraposition givesThis is the arithmetic statement of the second incompleteness theorem proved within PA: if PA is first-order consistent, there is no PA formal proof of its first-order consistency first-order sentence. The displayed implication is a PA theorem without assuming that PA proves its antecedent.

For the corresponding external consequence, if a first-order consistent PA proved ${\mathrm{Con}}_{PA}$, theoremhood would give a formal proof of its boxed assertion. The displayed theorem together with the supposed formal proof of first-order consistency gives its negation, contradicting first-order consistency. Hence an externally first-order consistent PA does not prove its own first-order consistency.

All implications in this argument are theorems of the extension $S$. From $Y\to (\square Y\to X)$, necessitation and normal modal distribution giveAxiom4 gives $\square Y\to \square \square Y$, soUnder the additional propositional antecedent $\square X\to X$, this theorem implies $\square Y\to X$. The reverse half of the fixed-point equivalence, $(\square Y\to X)\to Y$, consequently gives the theoremNecessitate that theorem and apply distribution to obtain $\square (\square X\to X)\to \square Y$. Combining with $\square Y\to \square X$ provesNecessitation was applied to a theorem after its propositional antecedent had been incorporated, never directly to a temporary assumption.

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.

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.

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

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.

Let $d(n)$ be the Gödel number of the diagonal first-order sentence obtained by substituting $\bar{n}$ into the one-free-variable logical formula with code $n$, with an arbitrary default value on noncodes. By the assumptions and (c), this total function has a strong defining logical formula $D(x,y)$.

For the specified $F$, form the one-variable logical formulaLet $h$ be the Gödel number of $H$ and put $C=H(\bar{h})$. Then $d(h)=┌C┐$. Strong definability of a numerical function at this particular standard input givesSubstitution into the existential definition yieldsThe permitted equivalence between the source's two substitution notations identifies this with its requested fixed point. Bound variables are renamed when necessary before forming $H$, so the substitution is capture-free. This constructs one particular first-order sentence from the code of the logical formula which applies $F$ to its own diagonal output.

A logical formula $D(\vec{x},y)$ weakly defines a total numerical function $f$ in $S$ if, for every standard input tuple $\vec{n}$ and $m=f(\vec{n})$,Strong definability of a numerical function additionally requires the internal uniqueness statementTogether with the positive instance, this is equivalent to proving $\forall y(D(\overline{\stackrel{⃗}{n}},y)\leftrightarrow y=\bar{m})$ for each standard input. The universal quantifier is the extra strength: it covers nonstandard potential outputs in first-order models of $S$. These are the weak and strong function conventions used here. ^[ref]

Suppose the graph of the total function is Sigma-1. Its complement is also Sigma-1, sinceReplace the graph assertion on the right by its Sigma-1 definition; existential quantifiers can be collected into one block. Bounded completeness of an arithmetic theory supplies numeralwise stage enumerators for each of these two disjoint complementary sets. Apply (b) to them. Its separating logical formula is provable exactly at the required graph tuples in the positive direction and refutable at all the other standard tuples, proving weak definability of a numerical function.

Using the graph logical formula alone would only supply positive instances from true existential witnesses; the separation construction is what supplies the negative-instance formal proofs without assuming Sigma-1 soundness or completeness for false Sigma-1 statements.

Write $H(\vec{v})$ for the proposed stage-comparison logical formula and fix a standard tuple $\vec{a}$. If $\vec{a}\in A$, numeralwise enumeration in arithmetic supplies a standard $m$ with $S⊢F(\overline{\stackrel{⃗}{a}},\bar{m})$. Disjointness gives $\vec{a}\notin B$, so $S⊢\neg G(\overline{\stackrel{⃗}{a}},\bar{j})$ for every standard $j$, in particular $j=0,\dots ,m$. The source's finite initial-segment axiom combines this finite list intoUse $\bar{m}$ as the existential witness to obtain $S⊢H(\overline{\stackrel{⃗}{a}})$.

If instead $\vec{a}\in B$, choose $n$ with $S⊢G(\overline{\stackrel{⃗}{a}},\bar{n})$. Disjointness gives refutations of $F(\overline{\stackrel{⃗}{a}},\bar{j})$ for all $j$, so the finitely many $j\le n$ giveFor an arbitrary $x$, the source's comparison axiom gives $x\le \bar{n}$ or $\bar{n}\le x$. In the first case the first conjunct of the proposed witness condition is false. In the second case $y=\bar{n}$ witnesses failure of its bounded universal conjunct, since $G(\overline{\stackrel{⃗}{a}},\bar{n})$ is provable. Generalization over $x$ therefore gives $S⊢\neg H(\overline{\stackrel{⃗}{a}})$.

Thus the logical formula separates $A$ from $B$. The formal proof uses the enumerators' numeralwise positive and negative formal proof properties and the two explicit order principles supplied in the source; it does not assume the first-order theory can decide arbitrary unbounded existential logical formulas.

A logical formula separates $A$ from $B$ in $S$ if it is provable at the standard numeral tuple of every member of $A$ and refutable at that of every member of $B$:There is no obligation on tuples outside the two sets. In a first-order consistent first-order theory these two obligations make $A$ and $B$ disjoint.

Let $h$ be the Gödel number of $H(v_1)$ and take the literal diagonal first-order sentence $R=H(\bar{h})$. If $S⊢R$, then $h$ belongs to the second source set, so separation gives $S⊢\neg H(\bar{h})$, a contradiction. If $S⊢\neg R$, then $h$ belongs to the first source set, so separation gives $S⊢H(\bar{h})$, again a contradiction. HenceThe direction of separation matters: here $H$ is provable on refutable diagonal codes and refutable on provable diagonal codes.

Start with the supplied bounded-complete, one-consistent first-order theory $T$ proving a false first-order sentence $F$. Replace it by its deductive closure, which preserves these properties and contains $F$. Enumerate the arithmetic first-order sentences as $X_0,X_1,\dots$. Recursively extend the current first-order theory by either $X_n$ or $\neg X_n$, choosing an extension which remains one-consistent as permitted by the supplied lemma, and then take its deductive closure. Call the resulting increasing sequence $T_n$, with $T_0$ the initial first-order theory, and put $S={\bigcup }_n{T}_n$.

Every stage is still bounded-complete. By (b), every stage has Sigma-1 soundness. If $S$ proved a false Sigma-1 first-order sentence, the finite formal proof would use assumptions from one stage $T_n$, contradicting its Sigma-1 soundness. Thus $S$ has Sigma-1 soundness and is bounded-complete, so (b) makes it one-consistent.

This soundness of an arithmetic theory argument is essential: the definition of one-consistency involves infinitely many standard refutations, so it would be insufficient merely to say that a violation has a finite formal proof. What has a finite formal proof is the false existential sentence, and bounded completeness of an arithmetic theory is what turns one-consistency into the needed soundness of an arithmetic theory condition.

The union is deductively closed because each formal proof has finitely many assumptions. It contains either $X$ or $\neg X$ for every first-order sentence, by the numeralwise enumeration in arithmetic, and contains the false first-order sentence $F$. If it were omega-consistent, (c) would make it correct on all first-order sentences, contradicting $F$. We have therefore constructedOmega-consistency always implies one-consistency by restricting its matrices. This counterexample proves that the converse is strictly false.

Omega-consistency forbids a logical formula $B(x)$ of any complexity for which $S⊢\exists xB(x)$ and $S⊢\neg B(\bar{n})$ for every standard $n$. The difference from one-consistency is that the matrix is unrestricted. It implies first-order consistency.

For a complete first-order consistent classical first-order theory, theorem membership obeys the ordinary Boolean truth tables. For example, it proves a conjunction exactly when it proves both conjuncts; completeness and first-order consistency also make theoremhood of a negation the complement of theoremhood of the first-order sentence. Omega-consistency additionally gives the witness propertyThe reverse implication is existential introduction. For the forward implication, if no standard instance were provable, completeness would give a formal proof of each negated instance, violating omega-consistency. This works also after replacing additional free variables by numerals.

Now induct on logical formulas with their remaining free variables replaced by standard numerals. At the atomic level, the equivalence between theoremhood and standard truth follows from bounded completeness of an arithmetic theory and bounded soundness of an arithmetic theory from (b). The Boolean steps use the truth-table facts just proved. The existential step uses the witness property and the induction hypothesis on its matrix; universal quantification follows by negation. Hencefor every first-order sentence $X$. Completeness ensures it decides each first-order sentence, and this equivalence ensures every decision is correct.

Bounded completeness of an arithmetic theory means that every bounded arithmetic first-order sentence true in the standard natural numbers is provable in $S$. If $S$ is first-order consistent and proves a false bounded arithmetic sentence $B$, bounded completeness of an arithmetic theory also proves its true bounded negation, a contradiction. Conversely, if every bounded theorem is true, $S$ cannot be inconsistent, because inconsistency would prove the false bounded arithmetic sentence $0=1$. ThusIf $S$ is one-consistent and proves $\exists xB(x)$ with bounded matrix, that existential sentence cannot be false: otherwise every $\neg B(\bar{n})$ would be a true bounded arithmetic sentence and hence provable, contrary to one-consistency. Thus $S$ has Sigma-1 soundness.

Conversely, Sigma-1 soundness excludes inconsistency. If $S⊢\exists xB(x)$, it supplies a standard witness $n$ with $B(n)$ true. Bounded completeness of an arithmetic theory proves $B(\bar{n})$, so first-order consistency forbids a formal proof of $\neg B(\bar{n})$. Hence there cannot simultaneously be refutations of all standard instances. ThereforeFinite blocks of existential logical variables are treated as finite tuples of witnesses, with the same argument.

On the first quadrant choose the holomorphic logarithm with $0<\arg w<\pi /2$. It maps $w=\rho e^{i\theta }$ to $\log \rho +i\theta$, so its image is precisely the strip $0<\mathrm{Im}\zeta <\pi /2$. Its inverse there is the exponential function; both derivatives are nonzero. Composing with part (i) givesThis is a bijective conformal map from the lens onto the strip, with inverseThe logarithm's branch is fixed by its argument range on the quadrant. Using a different branch would shift the strip vertically by an integer multiple of $2\pi$. This is the lens-to-strip logarithmic conformal map.

The first region is the lens around zero bounded by the two circular arcs through $-1$ and $1$. Writing $z=x+iy$, its inequalities combine to $x^2+y^2+2|y|<1$. The second region is the open first quadrant, and the third is the open horizontal strip between imaginary parts zero and $\pi /2$.

Set $t=(1+z)/(1-z)=u+iv$. The inverse is $z=(t-1)/(t+1)$, andHence the lens condition is exactly $u>|v|$. Multiplying by $1+i$ gives real part $u-v$ and imaginary part $u+v$, both positive exactly under that condition. Thereforeis a Möbius transformation mapping the lens bijectively to the first quadrant. Its pole at one lies on the boundary, and its inverse is $z=(w-(1+i))/(w+(1+i))$, well-defined throughout the quadrant. The derivative $2(1+i)/(1-z{)}^2$ never vanishes in the lens. This is a lens-to-quadrant Möbius map.

Treat a straight line together with infinity as a generalized circle on the Riemann sphere. Its finite points have a real equationTranslations and nonzero complex scalings preserve circles and lines. Under $z=1/w$, multiplying the equation by $|w{|}^2$ givesagain the equation of a circle or line. Nondegeneracy is preserved because the reciprocal map is a bijection of the sphere. The zero and infinite points are interpreted there, rather than discarded when multiplying denominators.

Every Möbius map with $c\ne 0$ factors asif $c=0$ it is already affine. Thus Möbius translation-scaling-inversion factorization and the reciprocal transformation of a generalized circle prove every generalized circle maps to another generalized circle. A circle becomes a line exactly when its image contains infinity, that is, when the original circle contains the map's pole.

For a holomorphic map, conformality means preservation of oriented angles locally; it holds at every point of $G$ exactly when $f^{\prime }(z)\ne 0$ there. A Möbius transformation is $M(z)=(az+b)/(cz+d)$ with $ad-bc\ne 0$, extended to the Riemann sphere at its pole and at infinity.

For three distinct finite points definewhich sends $z_1,z_2,z_3$ to $0,1,\infty$. If one point is infinite, take the corresponding limit: for $z_3=\infty$ use $(z-z_1)/(z_2-z_1)$; for $z_1=\infty$ use $(z_2-z_3)/(z-z_3)$; for $z_2=\infty$ use $(z-z_1)/(z-z_3)$. Construct $T_w$ similarly. Then $M=T_w^{-1}\circ T_z$ has the required three images.

For uniqueness, normalize any two proposed maps by these same transformations. Composing one normalized map with the inverse of the other fixes $0,1,\infty$. A Möbius map fixing infinity has $c=0$, one fixing zero then has $b=0$, and fixing one forces $a=d$ up to the irrelevant common nonzero scalar. It is the identity. This proves sharp three-transitivity of Möbius transformations.

Use the upper half-disc of radius $R$, with a clockwise semicircular indentation of radius $\epsilon$ above zero. The integrand is holomorphic inside that indented contour, so its total integral is zero. On the large arc,because $a+b>0$, $a-b>0$ and $\mathrm{Im}z\ge 0$. Its integral has modulus at most $\pi /R$ and vanishes as $R\to \infty$.

On the small clockwise arc, $f(z)=b/z+O(1)$, so the integral tends to $-i\pi b$. Therefore the remaining real-axis integral satisfiesThe imaginary part is even and is an ordinary absolutely convergent integral: near zero its integrand tends to $ab$, and at infinity it is $O(x^{-2})$. Taking imaginary parts givesThe complex integral needs the Cauchy principal value because its real part has a $b/x$ singularity; the requested sine-product integral does not. This sine-product integral with inverse-square weight is an application of the upper-half-plane indentation rule.