Foundation Primitive Recognition Calculus Prcset Theory Parse Hf System Not Dege

The non-degenerate parse

In mathematics, the hereditarily finite sets are the sets that can be built 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. They form a miniature universe of sets, one that contains all finite mathematics. A standard way to encode them as natural numbers is Ackermann coding, where the number n represents a set whose members are exactly the positions of the 1-bits in the binary expansion of n. The empty set becomes 0, and the set containing the empty set becomes 1.

This coding satisfies the defining axiom of set theory, extensionality: two sets are equal exactly when they have the same members. In the coding, that means two natural numbers are equal exactly when their bits agree at every position, a fact the framework's machine-checked library of formal theorems proves. The library also proves that 0 has no members, that 1 has exactly one member, namely 0, and that two codes are distinguished exactly when they differ in some member. The coding therefore discriminates by genuine set difference, not by an artifact of the representation.

In Recognition Science, the framework models recognition events as a discrete ledger, a record of distinctions. A formal system in this framework is a structure with tokens, expressions, and a discrimination relation. The declaration hfSystem_not_degenerate establishes that the hereditarily finite sets, parsed into this formal system, are non-degenerate: they fall on the side of the distinction dichotomy that realizes the δ core, a minimal recognition structure. The proof is a theorem in the framework's library, derived from the fact that the hereditarily finite sets embed the δ core. The endpoints of the system are the empty set and its singleton, the von Neumann numerals 0 and 1, distinguished as sets.

The declaration does not claim that this coding is the only way to represent sets, nor that it is the most efficient. It does not claim that the hereditarily finite sets are the only non-degenerate formal system, nor that they are the most expressive. It does not claim that the framework's model of recognition events is the only possible one. What it establishes is a precise, machine-checked fact: the hereditarily finite sets, under the standard Ackermann coding, provide a non-degenerate foundation for the framework's recognition calculus.

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

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

What this page does not claim

This is not a claim that the hereditarily finite sets are the only non-degenerate formal system. This is not a claim that the Ackermann coding is the most efficient or natural way to represent sets. This is not a claim that the framework's model of recognition events is the only possible model.

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: