Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 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.

A diagonal substitution worked symbolically

Example

Take ψ(y)≡(y=y) in the diagonal construction. With D representing the diagonal substitution function d, let η(x)=∃y(D(x,y)∧y=y), e=#η, and θ=η(eˉ). Then d(e)=#θ and Q proves θ↔⌜θ⌝=⌜θ⌝.

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 θ↔ψ(⌜θ⌝). The construction is effective and requires neither consistency nor soundness.

Verification

Given: The explicit tautological psi and the fixed diagonal construction with its representing graph D.

1.1

The substitution operation in F1 takes the formula eta with its designated x place and inserts the numeral eˉ. Thus d(e)=#(∃y(D(eˉ,y)∧y=y))=#θ. Here e is a natural number, eta is a formula, and the inserted eˉ is a term; none is identified with the other. The unique-value property used in F1 gives Q⊢D(eˉ,y)↔y=⌜θ⌝.

F1given
2.1

If theta holds, choose its y witness; the equation in step 1.1 replaces y with the numeral of theta, yielding that numeral equal to itself. Conversely that reflexive equality and D(eˉ,⌜θ⌝) give the existential theta. Thus in this concrete instance Q proves theta, as well as the displayed biconditional. The calculation is independent of which fixed token numbering produces the numerical value e.

step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 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