TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Löb theorem

Statement

Let T have its own arithmetized syntax and a provability predicate ${Prov}_{T}$ satisfying D1–D3. Assume the diagonal lemma holds internally in the T-language for the formula ${Prov}_{T} (v) \to ϕ$ : there is a T-sentence $θ$ such that

$T ⊢ θ \leftrightarrow ({Prov}_{T} (⌜ θ ⌝) \to ϕ) .$

This hypothesis holds when T is in an effective signature extending Q by the diagonal lemma below. If $T ⊢ {Prov}_{T} (⌜ ϕ ⌝) \to ϕ$ , then $T ⊢ ϕ$ . Consistency is not a hypothesis. An interpretation of arithmetic suffices only after it supplies this exact unguarded T-language fixed point and identifies the displayed predicate with T's chosen provability predicate.

Facts & Assumptions

[F1]

The syntactic diagonal lemma: For every formula $ψ (v)$ with no other free variables in an effective signature extending arithmetic, there is a sentence $θ$ such that Q in that signature proves $θ \leftrightarrow ψ (⌜ θ ⌝)$ . The construction is effective and requires neither consistency nor soundness.

[F2]

Derivability conditions for the chosen proof predicate: For the standard certified predicate of an effective T extending PA, the following hold for sentences $ϕ, ψ$ : D1, if $T ⊢ ϕ$ then $T ⊢ {Prov}_{T} (⌜ ϕ ⌝)$ ; D2, T proves ${Prov}_{T} (⌜ ϕ \to ψ ⌝) \to ({Prov}_{T} (⌜ ϕ ⌝) \to {Prov}_{T} (⌜ ψ ⌝))$ ; D3, T proves ${Prov}_{T} (⌜ ϕ ⌝) \to {Prov}_{T} (⌜ {Prov}_{T} (⌜ ϕ ⌝) ⌝)$ . The interpreted version requires an effective PA copy and verification there of the arithmetic proof constructors and axiom-proof translations used below.

Proof

Given: The stated internal fixed point, D1–D3, and a T proof of $□ ϕ \to ϕ$ .

1.1F1F2given

Write $□ A$ for ${Prov}_{T} (⌜ A ⌝)$ . The hypothesis gives $θ \leftrightarrow (□ θ \to ϕ)$ ; when T extends Q in an effective signature, F1 supplies precisely this fixed point. D1 and D2 of F2 applied to its forward implication give $□ θ \to □ (□ θ \to ϕ)$ .

2.1F2step 1.1given

D3 gives $□ θ \to □ □ θ$ . D2 applied to $□ θ \to ϕ$ gives $□ (□ θ \to ϕ) \to (□ □ θ \to □ ϕ)$ . Combining these with step 1.1 yields $□ θ \to □ ϕ$ . The assumed reflection instance $□ ϕ \to ϕ$ therefore yields $□ θ \to ϕ$ .

3.1F2step 1.1step 2.1∎

The reverse fixed-point implication now gives theta as a T theorem. D1 gives $□ θ$ , and MP with step 2.1 gives phi. This proves the claim without appealing to second incompleteness.

Depends on

Used by

Second incompleteness for standard provability Theorem

Dependency tree · two levels

7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Moschovakis, Lecture Notes in Logic (2014) — 4C.9–4C.10 pp153–154; local direct D1–D3 proof, not the source's second-incompleteness route (standard reference, not scraped)
Avigad, Computability and Incompleteness (2007) — Theorem 4.8.1, pp115–116, complete formal derivation (standard reference, not scraped)