Relative Consistency via the Constructible Universe

This Lean 4 project is the model-parametric continuation of lean-constructible-universe. The upstream project constructs the concrete ZFSet universe LCarrier and proves

LCarrier models ZFC + V = L + GCH

This repository addresses the separate relative-consistency problem: starting from an arbitrary, possibly externally ill-founded model M of ZF, construct the internal class L^M and prove that its induced membership structure models ZFC + V = L + GCH.

Current status

The model-parametric construction and its semantic relative-consistency endpoint are complete. The checked development includes:

• all ZF set operations and both axiom schemes inside an arbitrary model, together with exact formula relativization to definable class subtypes;

• an internally coded D/E/Df/DefInternal evaluator, including the nonstandard-omega arithmetic needed in an externally ill-founded model;

• exact internal constructible stages, their canonical well-orders, and InnerLCarrier M;

• proofs that InnerLCarrier M satisfies full ZFC and the parameter-free exact-stage sentence textbookVEqualsLSentence;

• finite-formula Reflection, a set-coded Skolem hull, an internally represented Mostowski collapse, and evaluator transport through that collapse;

• standard-strength Condensation for the resulting hull:

  TextbookExactStageAt (internalOrdinalPart range) range

• internally represented order types, Hartogs ordinals, cardinal arithmetic, Cantor--Schroeder--Bernstein, and constructible-stage cardinal bounds;

• the parameter-preserving GCH argument: for every internal infinite cardinal kappa and every internal x subset kappa, the transitive seed insert x (successor kappa) is fixed by the collapse and places x in L_(Hartogs(kappa));

• internally represented injections P(kappa) -> Hartogs(kappa) and Hartogs(kappa) -> P(kappa), yielding GCH and hence CH in InnerLCarrier M;

• an input-dependent model transformation

  ZF.ModelType ->
    ZFCWithTextbookVEqualsLAndGCH.ModelType

  and the semantic relative-consistency endpoints

  ZF.IsSatisfiable ->
    ZFCWithTextbookVEqualsLAndGCH.IsSatisfiable
  
  ZFC.IsSatisfiable -> ZFCWithGCH.IsSatisfiable
  ZFC.IsSatisfiable -> ZFCWithCH.IsSatisfiable

Here ZFCWithCH and ZFCWithGCH are literal definitions ZFC ∪ {chSentence} and ZFC ∪ {gchSentence}. The final transfer never returns a fixed external ZFSet model; its output is the internal constructible carrier of the supplied model.

The V = L component deliberately uses textbookVEqualsLSentence, whose semantics is membership in an internally represented exact constructible stage. The project does not silently identify this sentence with the upstream project's separately defined vEqualsLSentence in arbitrary nonstandard models.

These are semantic satisfiability implications. A syntactic statement written with a particular proof calculus as Con(T) -> Con(T') additionally requires that calculus's soundness and completeness bridge.

The mathematical route and the checks required before each major theorem are recorded in TEXTBOOK_ROUTE.md. The primary reference is Wang Fangting, Axiomatic Set Theory, especially the constructibility, reflection, Skolem-collapse, and GCH development in Chapter 6. Exact scanned page references and the distinction between the textbook route and additional standard results are recorded in TEXTBOOK_CROSSWALK.md.

Dependency

The project pins the verified upstream development at commit 7f5a7d0 and uses the same Lean toolchain.

Build

lake update
lake --wfail build

Author

Zike Liu