Löb's theorem states that, for a first-order theory with the stated provability and diagonalization properties,
where . It does not require an extra consistency assumption.
By the diagonal lemma, choose with . necessitation rule and distribution applied to give
Using positive introspection gives the unconditional theorem . If , it follows that , and the reverse fixed-point implication gives . Necessitating gives , hence and finally .
The same derivation also gives the Internal form of Löb's theorem, needed for modal soundness. Put . From the unconditional , propositional reasoning and the fixed point give . necessitation rule and distribution imply , and hence
This internal statement was derived without necessitating a temporary assumption.
Let and assume is consistent. The allowed arithmetizations of the previous equivalences give
Suppose . Its contrapositive is , and the Hilbert-Bernays-Löb derivability conditions then give
Combining with the two internal equivalences yields . Since contains , it would prove , contrary to the given Gödel second incompleteness theorem for this consistent extension. Hence
Together 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 . The permitted arithmetized positive half of the Rosser sentence argument is
Pure first-order logic gives : if there is no proof of , each antecedent in its defining universal implication is false. Therefore
This uses the supplied internal Rosser implication, rather than replacing an external nonprovability fact by an unproved internal first-order sentence.
If is inconsistent, it proves by explosion. Conversely, suppose is consistent and, towards a contradiction, has a proof of with standard code . Consistency excludes any proof of . In particular, for each , the closed bounded statement is true and is provable in by Sigma-1 completeness. The true bounded statement is also provable.
Using the given finite-numeral exhaustion below , these finitely many nonproof facts give
For arbitrary , the given comparison splits into or . In the first case the antecedent is false. In the second case the known negative proof at code supplies the required witness . Hence proves
The Rosser sentence equivalence now gives , contradicting consistency. Thus
Only a fixed finite list of closed bounded facts was used; no assumption that the first-order theory is omega-consistent is needed.
Write and fix a refutable first-order sentence , so and . First prove the internal equivalence
Because is provable, the derivability conditions give . The fixed-point equivalence therefore yields .
For the reverse implication, necessitating and applying distribution gives . positive introspection gives . Finally the provable implication , necessitated and distributed, gives
Consequently , so . The same argument works with any chosen refutable first-order sentence in place of ; their formal consistency statements are provably equivalent.
By the classical deduction theorem for propositional logic applied to adjoining a first-order sentence, is consistent exactly when . The displayed equivalence makes and deductively equivalent. Therefore
No soundness assumption on that extension is being substituted for consistency.
Write , with the corner notation understood as the numeral for the Gödel number. An arithmetical provability predicate numerates the theorems of 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 to .
Here numerates the theorem set by the given assumption. If , its proof supplies a genuine natural-number witness, making a true Sigma-1 formula. Sigma-1 completeness gives , proving the first condition. The second condition is supplied explicitly. Since is itself a Sigma-1 formula, the given formalized Sigma-1 completeness yields , the third condition. Thus the specified existential proof predicate is an arithmetical provability predicate.
Given , choose the hyperplane divisors as in (a). The ratios form a linear subspace of by (d), and its dimension equals by (b). A linear subspace of a finite-dimensional vector space with the same dimension is the whole space. Hence for some homogeneous polynomial of degree , giving
The zero function corresponds to . 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 and . 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 . Locally the pole order cannot exceed the zero order of , whose divisor is . Thus .
Equality of two ratios is equivalent to vanishing on . 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 . One can also see this using Bézout's theorem: a homogeneous polynomial not divisible by has only finitely many intersections with , so cannot vanish on the whole curve. Consequently
Multiplication by the nonzero polynomial is injective. The linear map therefore has kernel and image dimension
The assumption makes both polynomial-space dimensions applicable directly.
The monomials with nonnegative integers form a basis for the vector space of homogeneous polynomials of degree . For each , there are choices of . Hence
The divisor has degree . The hypothesis gives . A divisor of negative degree has no nonzero section: if , then would be effective, but its degree would be negative because the divisor of a meromorphic function has degree zero. Thus . The Riemann-Roch theorem now gives
A meromorphic function on a compact Riemann surface has finitely many poles, say of orders . For each , choose a projective line through it that does not contain . Its hyperplane divisor contains with multiplicity at least one. Include copies of this divisor. The sum then dominates the pole divisor of .
Add further arbitrary hyperplane divisors until their number satisfies and . Adding effective divisors cannot destroy the pole bound, so for we have
For a constant function, including zero, no initial poles need to be covered; simply add sufficiently many lines.
Take and the chosen . Then , so , and . In affine coordinates the chosen lift becomes
Since is a primitive cube root of unity, . Three iterations fix and , whereas one does not. Thus
The other square-root choice replaces this map by . Its cube is , so that lift has order six. This sign dependence is why a lift was specified explicitly.
Both fix the point at infinity. In the complex torus model their linear multipliers have order three or six, so the lattice is stable under a primitive cube root and hence under . Choose a shortest nonzero period . The triangular lattice has covering radius : its equilateral triangles of side one each have circumradius . Approximating any period divided by by this lattice leaves a strictly shorter period, which must be zero. Therefore
Thus the cubic has the hexagonal lattice shape, independently of which of the two lifts is chosen.
At and , the chosen map is
The square is not the identity on the cubic, since a generic point has . Thus .
Choose the cubic's point as the origin in its complex torus description. Since fixes it, its torus form is , with . Exact order four implies ; . Therefore is stable under multiplication by .
To identify its shape without an unproved uniqueness assertion, choose a shortest nonzero period . For any , approximate by a Gaussian integer within distance . The difference belongs to and is shorter than , so it must vanish. Hence
The lattice is determined up to a nonzero complex scaling: it is square.
On the parameter, the two transformations are and . Their compositions yield
Every step lifts to an invertible projective transformation of the corresponding cubic curves. Therefore all six parameter values give isomorphic curves. Some values coincide for special ; this does not affect the conclusion.
Compose the preceding transformations, applying first and then . With the square-root convention already specified,
This invertible projective transformation fixes and carries to . It is important to retain the sign of the chosen lift on the coordinate when computing its order later.
An appropriate projective transformation is
It fixes and has an invertible representing matrix. For , , ,
Hence its restriction is an isomorphism .
Choose with . Since , the invertible diagonal projective transformation
fixes . Writing its image as , direct substitution gives
Thus it maps onto . Either choice of square root works. We choose at and at for the later order calculations.

Pinned article: Introduction to the OurBigBook Project

Welcome to the OurBigBook Project! Our goal is to create the perfect publishing platform for STEM subjects, and get university-level students to write the best free STEM tutorials ever.
Everyone is welcome to create an account and play with the site: ourbigbook.com/go/register. We belive that students themselves can write amazing tutorials, but teachers are welcome too. You can write about anything you want, it doesn't have to be STEM or even educational. Silly test content is very welcome and you won't be penalized in any way. Just keep it legal!
We have two killer features:
  1. topics: topics group articles by different users with the same title, e.g. here is the topic for the "Fundamental Theorem of Calculus" ourbigbook.com/go/topic/fundamental-theorem-of-calculus
    Articles of different users are sorted by upvote within each article page. This feature is a bit like:
    • a Wikipedia where each user can have their own version of each article
    • a Q&A website like Stack Overflow, where multiple people can give their views on a given topic, and the best ones are sorted by upvote. Except you don't need to wait for someone to ask first, and any topic goes, no matter how narrow or broad
    This feature makes it possible for readers to find better explanations of any topic created by other writers. And it allows writers to create an explanation in a place that readers might actually find it.
    Figure 1.
    Screenshot of the "Derivative" topic page
    . View it live at: ourbigbook.com/go/topic/derivative
  2. local editing: you can store all your personal knowledge base content locally in a plaintext markup format that can be edited locally and published either:
    This way you can be sure that even if OurBigBook.com were to go down one day (which we have no plans to do as it is quite cheap to host!), your content will still be perfectly readable as a static site.
    Figure 5. . You can also edit articles on the Web editor without installing anything locally.
    Video 3.
    Edit locally and publish demo
    . Source. This shows editing OurBigBook Markup and publishing it using the Visual Studio Code extension.
  3. https://raw.githubusercontent.com/ourbigbook/ourbigbook-media/master/feature/x/hilbert-space-arrow.png
  4. Infinitely deep tables of contents:
    Figure 6.
    Dynamic article tree with infinitely deep table of contents
    .
    Descendant pages can also show up as toplevel e.g.: ourbigbook.com/cirosantilli/chordate-subclade
All our software is open source and hosted at: github.com/ourbigbook/ourbigbook
Further documentation can be found at: docs.ourbigbook.com
Feel free to reach our to us for any help or suggestions: docs.ourbigbook.com/#contact