Foundation Primitive Recognition Calculus Prcset Theory Parse Hf System Embeds D

Set theory inside the ledger

Hereditarily finite sets are the sets you can build from the empty set using only the operations of pairing and union, with every element itself built the same way. They include the empty set ∅, the singleton {∅}, the pair {∅, {∅}}, and so on. Each such set can be assigned a natural number code, and the membership relation between sets becomes a simple bit test on those codes: a number i is a member of a code n exactly when bit i of n is set. This is the standard Ackermann coding, and it is the classical way to show that the hereditarily finite sets can be modeled inside arithmetic.

The Recognition Science framework works with a ledger, a discrete record of recognition events, and the theorem here shows that this ledger is not a narrow device. The declaration hfSystem_embeds_delta, proved in the framework's machine-checked library of formal theorems, establishes that the entire hereditarily finite set universe can be embedded into the ledger's formal system. The embedding preserves the key structure: two set codes are distinguished exactly when they differ in some member, which is the axiom of extensionality. The empty set is coded by 0, the singleton {∅} by 1, and the framework's endpoints, the two objects it uses to mark the start and end of a recognition trace, are exactly these two sets.

What this means in plain terms is that the ledger's basic discrimination relation, the relation that says two tokens are different, is not an arbitrary choice. It is the same relation as genuine set difference. The framework proves that its primitive recognition calculus contains the full hereditarily finite sets, which is the universe of sets that most of classical mathematics can be built from without needing infinite sets or choice. This is a structural result: the ledger is not a toy model but a system rich enough to express the foundations of arithmetic and finite set theory.

The theorem does not claim that the hereditarily finite sets are the only thing the ledger can express, nor that the embedding is unique, nor that the framework's recognition calculus is identical to set theory. It shows an embedding exists, not that the ledger is limited to set theory. The proof also does not claim anything about infinite sets, the axiom of choice, or the consistency of set theory itself. It is a precise, narrow result about how one foundational structure sits inside another.

/-- **HF set theory contains the δ core.** -/
theorem hfSystem_embeds_delta : Nonempty (PRCEmbeddingInto hfSystem) :=
  FormalSystemEmbeddingTarget_proved hfSystem hfSystem_expressive

/-- The discrimination relation IS the foundation's own extensional set inequality:
two codes are distinguished exactly when they differ in some member. So `hfSystem`
discriminates by genuine set difference, not by code accident. -/
theorem distinguishes_iff_extensional (a b : ℕ) :
    hfSystem.distinguishes a b ↔ ∃ i, ¬ (Mem i a ↔ Mem i b) := by
  show a ≠ b ↔ ∃ i, ¬ (Mem i a ↔ Mem i b)
  rw [ne_eq, ext_iff a b]
  push_neg
  rfl

/-- The empty set is coded by `0`: it has no members. -/
theorem not_mem_empty (i : ℕ) : ¬ Mem i 0 := by
  simp [Mem]

/-- The singleton `{∅}` is coded by `1`: its only member is `0 = ∅`. -/
theorem mem_one_iff (i : ℕ) : Mem i 1 ↔ i = 0 := by
  cases i with
  | zero => exact iff_of_true (by show Nat.testBit 1 0 = true; decide) rfl
  | succ j =>
      refine iff_of_false ?_ (Nat.succ_ne_zero j)
      have h2 : (1 : ℕ) / 2 = 0 := by decide
      simp [Mem, Nat.testBit_succ, h2]

What this page does not claim

The theorem does not claim the hereditarily finite sets are the only content of the ledger. The theorem does not claim anything about infinite sets, the axiom of choice, or the consistency of set theory. The theorem does not claim the embedding is unique.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCSetTheoryParse.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: