Ackermann coding: hereditarily finite sets as naturals (issue #19A)

The concrete carrier for the HF admissible presentation. a ∈ₐ b means bit a of b is set, so every natural is a finite set of naturals and the coding is total in both directions.

Why specification laws, not totality

A closure obligation stated as totality is vacuous:

  pair_total : ∀ a b, ∃ c, Pair a b c

is satisfied by Pair := fun _ _ _ => True on any inhabited carrier — totality is not pairing. Closure is meaningful only against an ambient membership relation together with specification laws saying which element the operation produces. This file supplies that membership for HF and proves the specifications hold.

Only pairing and union are built here. The full KP schema is deliberately not attempted: which closure and absoluteness laws are actually consumed is settled by the proofs that need them, and no such proof exists yet.

Main definitions

• Nat.AckMem (∈ₐ): Ackermann membership.
• Nat.ackPair, Nat.ackUnion: the witnessing constructions.

Main results

• Nat.mem_ackPair, Nat.mem_ackUnion: the specification laws — the content the bare totality fields lacked.
• Nat.ack_ext: the coding is extensional.
• Nat.finite_ackMem / Nat.exists_ack_of_finite: codes name exactly the finite sets of naturals. This is what will make A-finiteness coincide with ordinary finiteness at HF.

def Nat.AckMem (a b : ℕ) : Prop

Ackermann membership: a ∈ₐ b iff bit a of b is set.

Equations

• a.AckMem b = (b.testBit a = true)

def Nat.«term_∈ₐ_» : Lean.TrailingParserDescr

Ackermann membership: a ∈ₐ b iff bit a of b is set.

Equations

• Nat.«term_∈ₐ_» = Lean.ParserDescr.trailingNode `Nat.«term_∈ₐ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈ₐ ") (Lean.ParserDescr.cat `term 51))

theorem Nat.ackMem_def {a b : ℕ} : a.AckMem b ↔ b.testBit a = true

theorem Nat.ackMem_iff_mem_bitIndices {a b : ℕ} : a.AckMem b ↔ a ∈ b.bitIndices

@[instance_reducible]

instance Nat.instDecidableAckMem {a b : ℕ} : Decidable (a.AckMem b)

Equations

• Nat.instDecidableAckMem = Nat.instDecidableAckMem._aux_1

theorem Nat.ack_ext {a b : ℕ} (h : ∀ (x : ℕ), x.AckMem a ↔ x.AckMem b) : a = b

Codes with the same members are equal — Ackermann coding is extensional.

Pairing

def Nat.ackPair (a b : ℕ) : ℕ

The Ackermann code of the pair {a, b}.

Equations

• a.ackPair b = 2 ^ a ||| 2 ^ b

@[simp]

theorem Nat.mem_ackPair {a b x : ℕ} : x.AckMem (a.ackPair b) ↔ x = a ∨ x = b

The pairing specification. This is the law the bare pair_total field lacked.

Union

def Nat.ackUnion (a : ℕ) : ℕ

The Ackermann code of ⋃ a: bitwise-or of the members of a.

Equations

• a.ackUnion = List.foldr (fun (x1 x2 : ℕ) => x1 ||| x2) 0 a.bitIndices

@[simp]

theorem Nat.mem_ackUnion {a x : ℕ} : x.AckMem a.ackUnion ↔ ∃ (y : ℕ), y.AckMem a ∧ x.AckMem y

The union specification.

Finiteness — why A-finite will collapse to finite at HF

theorem Nat.finite_ackMem (a : ℕ) : {x : ℕ | x.AckMem a}.Finite

Every Ackermann code names a finite set.

theorem Nat.exists_ack_of_finite {s : Set ℕ} (hs : s.Finite) : ∃ (a : ℕ), ∀ (x : ℕ), x.AckMem a ↔ x ∈ s

…and conversely every finite set of naturals is named by a code.