新基础是一致的 - SegmentFault 思否

1937 & 2010: In 1937, Quine proposed "New Foundations" set theory. Since 2010, Randall Holmes claimed a proof of its consistency.
Proof Verification: Use Lean to verify the difficult part of Holmes' proof, proving New Foundations is consistent. The proof is in ConNF/Model/Result.lean, with source and docs.
More Info: See website, Lean code docs, and deformalisation paper. Also read the blueprint.
Running Code Locally: Install elan, clone repo, and run lake exe cache get in terminal. Code can be viewed in VS Code or compiled with lake build.
Objective: New Foundations is consistent if and only if Tangled Type Theory (TTT) is. Formally constructed a TTT model in Lean to prove Con(NF), working from Holmes' papers with alterations.
Tangled Type Theory: A many-sorted set theory with equality "=" and membership relation "∈", sorted by limit ordinal λ. Extensionality is an axiom, making model construction difficult.
Strategy:
- Base Type Construction: Use limit ordinal λ, regular ordinal κ > λ, and strong limit cardinal μ > κ. Construct an auxiliary base type with μ atoms partitioned into κ-sized litters.
- Constructing Each Type: At each type level α, produce t-sets and allowable permutations. T-sets have a support and preferred extensions.
- Controlling Type Size: Each type α is constructed under certain assumptions. Use the [freedom of action theorem] to show there are at most μ elements.
- Finishing Induction: Recursively produce types at all levels. Check construction produces a TTT model by satisfying a finite axiomatisation.
Dependency Graph: dependency graph or [depgraph.pdf] shows the project's dependencies.