TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Structural induction and recursion on syntax

Statement

Constructor induction is valid for the term and formula sets: a property true of leaves and preserved by each licensed constructor holds of every expression. For a specified set $A$ , supplied leaf values in $A$ , and supplied operations into $A$ for all constructors on the appropriate finite powers of $A$ , there is a unique evaluation $E : {Term}_{L} \cup {Form}_{L} \to A$ obeying those rules. The construction is uniform in the supplied parameters. Operations may also depend on the constructor's symbol fields.

Facts & Assumptions

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

[F1]

Every term and every formula in the delimited coding has exactly one outer constructor, with uniquely determined symbol fields and immediate subexpressions. Each immediate subexpression is shorter than its parent. (Unique parsing of finite syntax)

[F2]

Let $(N, 0, σ)$ be a Peano system (def-peano-system), in particular the natural numbers $N$ (def-natural-numbers). For any set $A$ , any element $a \in A$ , and any function $f : A \to A$ , there is a unique function $g : N \to A$ such that $g (0) = a$ and $g (σ (n)) = f (g (n))$ for all $n \in N$ . (The recursion theorem)

[F3]

Let $P$ be a property of naturals such that for every $n \in N$ , if $P (m)$ holds for all $m < n$ then $P (n)$ . Then $P (n)$ holds for all $n \in N$ . (At $n = 0$ the hypothesis is vacuous, so $P (0)$ is forced.) (Strong (complete) induction)

Proof

1.1

Immediate subexpressions are uniquely determined and shorter. Strong induction on word length therefore proves constructor induction, including the vacuous shorter-expression hypothesis at the first leaves.

F1F3

1.2

Let $D$ be the expression set and use the state set $B = ω \times P (D \times A)$ . Start with $(0, \emptyset)$ . For a state $(n, h)$ whose second component is the correct evaluation of expressions of length at most $n$ , extend $h$ to all expressions of length $n + 1$ using the prescribed operations and shorter child values. Leaves use their supplied values. On any other state set the successor state to $(n + 1, \emptyset)$ , making the rule a total set function $B \to B$ . Parsing gives a unique value at every newly added expression.

F1construct

2.1

Natural recursion in $B$ gives the state sequence. Induction on $n$ shows only correct states are reached and their graphs extend one another. Their union is a set function with domain $D$ obeying the rules. Any other evaluation agrees on leaves and then on a constructor whenever it agrees on its children, so step 1.1 proves uniqueness. The state definition uses only the given parameters, proving uniformity.

F2step 1.1step 1.2∎

Depends on

Used by

Free variables and free-for substitution Definition
Term denotation Definition
Skolem witness closure on a cardinal Lemma

Dependency tree · two levels

10 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) — Appendix app3–app5, pp.2–3. (standard reference, not scraped)