zfc.lean

namespace zfc

universe u

constant set : Type 1
constant is_element_of : set → set → Prop

local notation a `∈` b := is_element_of a b

def is_subset_of (a : set) (b : set) : Prop :=
  ∀ e : set, e ∈ a → e ∈ b

local notation a `⊆` b := is_subset_of a b


-- Axiom of Extensionality: Two sets that have the same elements are equal.
--
-- I gather "extensionality" is the property of not also meaning anything else.
-- (In mainstream programming terms: you can't subclass `set` and add fields;
-- if two sets agree on all the "base class" behavior, they are the same set.)
-- For example, Lean has an axiom `propext`, the extensionality of
-- propositions, that says that if `p ↔ q`, then `p = q`.
axiom extensionality : ∀ x y, (∀ z, z ∈ x ↔ z ∈ y) → x = y

-- Some notation used in the axiom of replacement.
local notation `∀` binders `∈` x `,` pred:(scoped P, P) := ∀ z, z ∈ x → pred z
local notation `∃` binders `∈` x `,` pred:(scoped P, P) := ∃ z, z ∈ x ∧ pred z
local notation `∃!` binders `∈` x `,` pred:(scoped P, P) := ∃! z, z ∈ x ∧ pred z

-- Axiom Schema of Replacement: The image of a set in a partial function is a
-- set.
--
-- Lean's use of lambda to represent functions and sets often indicates a break
-- with ZF, but here our use of lambda corresponds to how the axiom schema is
-- supposed to work: there's an instance for each *formula*, a countable set.
--
-- Literally: For every binary relation ϕ that maps each element of some set a
-- to a unique y, there exists a set b that is the image of a in ϕ.
axiom replacement :
  ∀ (ϕ : set → set → Prop) a,
    (∀ x ∈ a, ∃! y, ϕ x y) → ∃ b, ∀ y, y ∈ b ↔ ∃ x ∈ a, ϕ x y

-- Axiom Schema of Specification: Any definable subclass of a set is a set.
--
-- In programming terms, you can filter a set by a predicate, and the result is
-- a set. (In Metamath this is derived as a theorem, as Metamath's ax-rep
-- Axiom Schema of Replacement is strong enough to imply it.)
axiom specification :
  ∀ (θ : set → Prop) a, ∃ b, ∀ e, e ∈ b ↔ e ∈ a ∧ θ e

-- Axiom of Power Sets: For every set x, there is a set that contains all
-- subsets of x.
--
-- (This wording stops short of establishing that each subset, as we understand
-- the term, exists, but any subset of x that *does* exist is in the postulated
-- power set y.)
--
-- (This wording also does not exactly say that the postulated set y doesn't
-- contain other sets as well. Metamath style is economic to a fault. But the
-- axiom of specification can be used to eliminate anything else.)
axiom power_sets : ∀ x, ∃ y, ∀ z, z ⊆ x → z ∈ y

-- Axiom of Union: For every set x, the union of the sets in x exists.
axiom union : ∀ x, ∃ ux, ∀ z, (∃ e, z ∈ e ∧ e ∈ x) → z ∈ ux

-- Axiom of Regularity (Foundation): Every nonempty x contains a set that is
-- disjoint with x.
--
-- According to Wikipedia, some elementary consequences of this are: no set
-- contains itself; two sets cannot contain each other; every descending
-- sequence of sets a ∋ b ∋ c ∋ ... ends eventually.
--
-- This may also imply the law of the excluded middle. I don't know.
axiom regularity : ∀ x, (∃ y, y ∈ x) → ∃ y, y ∈ x ∧ ∀ z, z ∈ y → ¬ z ∈ x

-- Axiom of Infinity: The set of natural numbers exists. Metamath uses a
-- different ax-inf that is equivalent, shorter, and incomprehensible. It
-- proves this form as a theorem, axinf2.
axiom infinity :
  ∃ nat,
    (∃ e, e ∈ nat ∧ ¬∃ x, x ∈ e)  -- an empty set is in nat
    -- for all x in nat, the successor y of x is in nat
    ∧ ∀ x, x ∈ nat → ∃ y, y ∈ nat ∧ ∀ z, z ∈ y ↔ z ∈ x ∨ z = x

theorem null_set_exists : ∃ x, ∀ y, ¬(y ∈ x) :=
  have h1 : ∀ z, ∃ x, ∀ y, y ∈ x ↔ (y ∈ z ∧ y ∈ y ∧ ¬ y ∈ y),
  from specification (λ y, y ∈ y ∧ ¬ y ∈ y),
  have h2 : ∀ y, ¬(y ∈ y ∧ ¬(y ∈ y)),
  from λ y pair, pair.right pair.left,
  have h3 : ∀ z y, ¬(y ∈ z ∧ (y ∈ y ∧ ¬(y ∈ y))),
  from λ z y three, h2 y three.right,
  have h5 : ∀ x y z, (y ∈ x ↔ (y ∈ z ∧ y ∈ y ∧ ¬ y ∈ y)) → ¬(y ∈ x),
  from λ x y z hbi yx, h3 z y (hbi.mp yx),
  have h6 : ∀ z x, (∀ y, (y ∈ x ↔ (y ∈ z ∧ y ∈ y ∧ ¬ y ∈ y))) → ∀ y, ¬(y ∈ x),
  from λ z x hy y, h5 x y z (hy y),
  have h7 : ∀ z, (∃ x, ∀ y, (y ∈ x ↔ (y ∈ z ∧ y ∈ y ∧ ¬ y ∈ y))) → ∃ x, ∀ y, ¬(y ∈ x),
  from λ z ex, exists.elim ex (λ x h, exists.intro x (λ y, (h6 z x) h y)),
  have h8 : ∀ z, ∃ x, ∀ y, ¬(y ∈ x),
  from λ z, h7 z (h1 z),
  -- To dispense with the `∀ z`, we must produce some set. It doesn't matter
  -- which. Any set will do. Note that Metamath's proof (axnul), which we follow
  -- closely, does not need to do this, for reasons to do with free variables
  -- that I don't understand.
  infinity.rec_on (λ nat h, h8 nat)

-- Axiom of Choice: For every set x, there is a set y that selects one element
-- from each nonempty element of x.
--
-- In particular, for every set x, there exists a set y of pairs, such that for
-- each nonempty w in x, there is a unique "chosen" element v ∈ w such that
-- {w, v} ∈ y.
--
-- I imagine it turns out that these pairs are as good as ordered pairs if you
-- think it over (something I have not personally done).
axiom choice :
  ∀ x, ∃ y, ∀ z w, (z ∈ w ∧ w ∈ x) →
    ∃ v, ∀ u, (∃ pair, u ∈ w ∧ w ∈ pair ∧ u ∈ pair ∧ pair ∈ y) ↔ u = v

end zfc