Foundation Primitive Recognition Calculus Prcset Theory Parse

The set-theory parse

Hereditarily finite sets are the sets you can build from the empty set using only finitely many steps: the empty set itself, the set containing the empty set, the set containing that, and so on. A standard result, the Ackermann coding, represents each such set as a natural number by reading the number's binary digits as a membership table. Bit i of the code for set n is set exactly when set i is a member of set n. The empty set becomes 0, the set containing the empty set becomes 1, and every finite set gets a unique code.

The framework's library, a machine-checked collection of formal theorems, proves that this coding is faithful. Two codes are equal exactly when they have the same members, which is the axiom of extensionality. The code 0 has no members, and the code 1 has exactly one member, namely 0. The library also proves that the coding distinguishes two sets exactly when they differ in some member, so the discrimination relation is genuine set difference, not an accident of the code.

In Recognition Science, the primitive recognition calculus is the foundational ledger, a discrete record of events and their costs. The library's module parses hereditarily finite set theory into this calculus by treating set codes as tokens and the derivation-length order as the expression order. It then proves that this parsed system is expressive: it can distinguish its two endpoints, the empty set and its singleton. From that, the library derives that the set-theory parse realizes the δ core, the minimal expressive core of the recognition calculus, and that it is non-degenerate, meaning it does not collapse into a trivial system.

The consequence is that the framework's most primitive structure already contains the full expressive power of finite set theory. The recognition calculus does not need a separate axiom for sets; the natural numbers, with their binary structure, already provide it. This is a formal bridge from the ledger's minimal assumptions to the world of sets that classical mathematics builds on.

/-- **Extensionality.** Two HF codes are equal iff they have the same members. The
Ackermann interpretation satisfies the axiom of extensionality; it is exactly ℕ bit
extensionality. -/
theorem ext_iff (m n : ℕ) : m = n ↔ ∀ i, (Mem i m ↔ Mem i n) := by
  refine ⟨fun h i => by rw [h], fun h => Nat.eq_of_testBit_eq fun i => ?_⟩
  have hi := h i
  cases hm : Nat.testBit m i <;> cases hn : Nat.testBit n i <;> simp_all [Mem]

/-- 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]

/-- 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

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

/-- HF set theory falls on the δ side of the distinction dichotomy: it is
non-degenerate, hence realizes δ. -/
theorem hfSystem_not_degenerate : ¬ DistinctionDichotomy.Degenerate hfSystem :=
  DistinctionDichotomy.not_degenerate_of_realizesDelta hfSystem hfSystem_embeds_delta

What this page does not claim

This module does not prove that all of set theory, including infinite sets, can be encoded in the recognition calculus. The parse does not establish the physical recognition-to-linking bridge; that remains open. The Ackermann coding is a classical result, not a new theorem of the framework.

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: