Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14
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.

Blass's finite-modification classes and parameter-HOD model

Definition

Work in the metatheory with a countable transitive MZF+V=L. Thus M satisfies Choice by the canonical constructible well-order, and this is the only ambient source of Choice in the setup. Force over M with

P=Fn(ω×ω,2),

the finite partial functions ordered by reverse inclusion. If G is M-generic, define the mutually Cohen-generic reals

an={k<ω:(G)(n,k)=1}(n<ω).

For any real xω, its finite-modification class is

δ(x)={yω:xy is finite},

where is the symmetric difference of The difference ab, the symmetric difference ab, and the complement Xa relative to a set X. Put

f(n)={δ(an),δ(ωan)}

and

S=n<ω(δ(an)δ(ωan)){f}.

Blass's class N consists of all xM[G] such that every member of TC({x}) is uniquely definable in M[G] from f, finitely many members of S{f}, and finitely many ordinal parameters. This is the convention denoted HOD(S), or “HOD over S,” in the source. It is important that S acts as a reservoir of finitely many parameters, not as one pointwise named parameter: S is definable from the single permitted parameter f, while individual definitions may also use only finitely many reals from its displayed union.

The range

R=ran(f)={{δ(an),δ(ωan)}:n<ω}

is therefore a canonically enumerated family of pairs in N. The later term Blass model refers to this parameter-HOD class N. The ordinary HOD coding convention is that of Ordinal definability and HOD; the usual HOD inner-model proof from HOD as an inner model and comparison with L must be relativized to this finite-parameter reservoir before any ZF conclusion about N is used.

Depends on

Used by

Dependency tree · two levels

15 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