setFoundationSystem
plain-language theorem explainer
Packages classical set theory's first distinction (empty set versus the one-point universe) as a FormalSystem carrier for the PRC inevitability argument. Cited by anyone showing that set foundations realize the primitive distinction δ rather than collapsing. Built as a direct instance of the two-distinct-primitives constructor with the proof of ∅ ≠ univ.
Claim. The set-theoretic foundation is the formal system obtained from two distinct sets on a one-point domain: the empty set $\emptyset$ and the universe $\mathrm{Univ}$, using inequality of tokens as distinction and length order on natural numbers as expression extension.
background
Primitive Recognition Calculus (PRC) studies whether any non-degenerate formal system must realize a minimal distinction δ. The ambient interface is FormalSystem: carriers Token and Expr, a distinguishes relation on tokens, an exprExtends order on expressions, and a map from abstract endpoints to tokens.
The helper ofTwoDistinct builds such a system from any type with two unequal elements a₀ ≠ a₁. Tokens are the type's elements, distinction is inequality, expressions are natural numbers ordered by ≤, and the two endpoints land on a₀ and a₁.
Here the type is Set Unit. On a one-point domain, ∅ and univ are the set-theoretic stand-ins for 0 = ∅ and 1 = {∅} that open the von Neumann hierarchy; Set.empty_ne_univ supplies the required inequality.
proof idea
One-line definitional wrapper. Instantiate ofTwoDistinct at α = Set Unit with the pair (∅, univ) and the standard lemma Set.empty_ne_univ. No further proof obligations: the FormalSystem fields are filled by the constructor.
why it matters
Supplies the set-theory leg of the four named foundations. Downstream, setFoundationSystem_embeds_delta shows Nonempty (PRCEmbeddingInto setFoundationSystem) by two_distinct_realizes_delta on the same pair. That fact is conjoined in named_foundations_embed_delta (Item 4, widened): logic, Peano arithmetic, set theory, and type theory each realize the δ core, so the primitive distinction is not an artifact of one notation. It also feeds named_foundations_not_degenerate, placing set theory on the non-degenerate side of the PRC dichotomy. Within the Recognition forcing chain this is foundation-level scaffolding for inevitability, not yet a T5–T8 physics step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.