Foundation Primitive Recognition Calculus Prcset Theory Parse Distinguishes Iff

What set difference means

Set theory begins with a question of identity: when are two sets the same? The standard answer, called extensionality, is that two sets are equal precisely when they have the same members. A set with no members is the empty set; a set whose only member is the empty set is different from it. This principle is so basic that it often goes without saying, but in a formal system it must be stated and proved.

The Recognition Science framework's machine-checked library of formal theorems encodes this idea in a concrete way. It represents every set as a natural number, using a coding scheme where the bits of the number indicate membership. The number 0 codes the empty set, with no bits set; the number 1 codes the singleton containing the empty set, with only the first bit set. Membership of code i in code n simply means that the i-th bit of n is set to 1.

The declaration distinguishes_iff_extensional proves that this coding respects the fundamental set-theoretic notion of difference. In the framework's formal system, two codes are distinguished exactly when they differ in some member. This is not a new axiom or a special case; it is a theorem derived from the basic definition of membership as a bit test. The proof is short and direct: it unfolds the definition of distinction, applies the extensionality theorem for the coding, and pushes a negation through a universal quantifier.

What this establishes is that the framework's primitive recognition relation, the relation that tells two things apart, coincides with genuine set difference. Two sets are recognized as distinct by the system if and only if they are actually different sets. This is a foundational consistency check: the most basic operation of the framework, telling things apart, aligns with the most basic principle of set theory. It means the framework is not distinguishing codes by accidental features of their representation, but by the sets they represent.

This result does not claim that the framework derives all of set theory, nor that it proves the consistency of set theory. It does not claim that natural numbers are sets, only that they can code sets in a way that preserves extensional difference. It does not claim that the framework's notion of distinction is the only possible one. What it does is anchor the framework's primitive operation to a classical, well-understood mathematical structure, showing that the framework's basic machinery is compatible with standard set theory from the ground up.

/-- 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 framework does not derive all of set theory from this single theorem. The framework does not claim that natural numbers are sets, only that they can code them. The framework does not claim its notion of distinction is the only possible one.

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: