πŸ“₯ Download raw
module Padova2025.Explorations.CZF where

Sets as trees

open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProvingBasics.Negation
open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.ProvingBasics.Connectives.Conjunction
open import Padova2025.ProvingBasics.Termination.Gas
open import Agda.Primitive

Set theory and type theory in all their flavors can both be used as foundations for large parts of mathematics. And they are interconnected: Within set theory, we can build models of type theory, and within type theory, we can build models of set theory. The latter is the purpose of this module: We will introduce a type V whose elements represent sets as in set theory. We will have constants like βˆ… (representing the empty set) and N (representing the set of natural numbers), functions like union (for taking the union of a set of sets), a global membership relation called _∈_, and so on. We will then also be able to study the properties of this model of set theory: Does the axiom of choice hold? The powerset axiom?

The model we will describe is Peter Aczel’s sets as trees model. We represent sets by arbitrarily-branching trees; for instance, the set { x, {y,z}, {0,1,2,...} } is represented by the following tree:

         *
        β•±β”‚β•²
       β•± β”‚ β•²
      β•±  β”‚  β•²
     β•±   β”‚   β•²
    β•±    β”‚    β•²
   x     *     *
        β•± β•²   β•±β”‚β•²
       y   z 0 1 2 ...

In Agda, we express this idea as follows.

data V : Set₁ where
  sup : {I : Set} β†’ (I β†’ V) β†’ V

The constructor sup takes an indexing type I and an I-indexed family of trees and returns a new tree with those trees as the children of its root. In the beginning, we do not know any trees; to get off the ground, we use the empty family of trees:

βˆ… : V
βˆ… = sup {βŠ₯} empty-function   -- just a root node without children
  where
  empty-function : βŠ₯ β†’ V
  empty-function ()

Given trees x and y, we can create a new tree whose root has x and y as its children:

pair : V β†’ V β†’ V
pair x y = sup {Bool} f  -- a root node with two children
  where
  f : Bool β†’ V
  f false = x
  f true  = y

The following function is supposed to map a set x to the singleton set { x }, i.e.Β a tree x to a tree whose root has exactly one child, namely x.

singleton : V β†’ V
singleton = {!!}

The following function is supposed to input two sets x and y and output the ordered Kuratowski pair { {x}, {x,y} }.

kuratowski : V β†’ V β†’ V
kuratowski = {!!}

For some results below, the following two projection functions are nice to have. They allow us to access the indexing type or the family without having to pattern match on the set in question.

Index : V β†’ Set
Index (sup {I} f) = I

fam : (x : V) β†’ Index x β†’ V
fam (sup {I} f) = f

The set-theoretic natural numbers

In set theory, the natural numbers are often bootstrapped from the empty set as follows.

0 ≔ {}
1 ≔ { 0 }       = { {} }                  = 0 βˆͺ {0}
2 ≔ { 0, 1 }    = { {}, {{}} }            = 1 βˆͺ {1}
3 ≔ { 0, 1, 2 } = { {}, {{}}, {{},{{}}} } = 2 βˆͺ {2}

In other words, a number is identified with its set of predecessors; the number zero does not have any predecessors and is hence represented by the empty set. To mimic this construction in Agda, let us implement the function next which inputs a set X and outputs X βˆͺ {X}.

next : V β†’ V
next = {!!}

With next in place, we can convert every actual natural number into its set-theoretic representation…

fromβ„• : β„• β†’ V
fromβ„• = {!!}

…and thereby obtain the set of natural numbers:

N : V
N = sup {β„•} fromβ„•

An equivalence relation

In set theory, the sets { x, y } and { y, x } are deemed equal; however, in Agda, the trees pair x y and pair y x are distinct:

  *           *
 β•± β•²   vs.   β•± β•²
x   y       y   x

We hence need to introduce an equivalence relation _β‰ˆ_ expressing that two trees represent the same set.

infix 4 _β‰ˆ_
_β‰ˆ_ : V β†’ V β†’ Set
sup {I} f β‰ˆ sup {J} g =
  ((i : I) β†’ βˆƒ[ j ] (f i β‰ˆ g j)) Γ—
  ((j : J) β†’ βˆƒ[ i ] (g j β‰ˆ f i))
-- "Every child `f i` is equivalent to one of the children of `sup g`,
-- and vice versa."

β‰ˆ-refl : {x : V} β†’ x β‰ˆ x
β‰ˆ-refl = {!!}

β‰ˆ-sym : {x y : V} β†’ x β‰ˆ y β†’ y β‰ˆ x
β‰ˆ-sym = {!!}

β‰ˆ-trans : {x y z : V} β†’ x β‰ˆ y β†’ y β‰ˆ z β†’ x β‰ˆ z
β‰ˆ-trans = {!!}

The membership relation

Fundamental to set theory is the membership relation ∈. This relation is also responsible for one of the most discernible differences between set theory and type theory: In set theory, for any two sets X and Y, the expression β€œXβ€„βˆˆβ€„Y” is always a well-defined assertionβ€”perhaps provable, perhaps refutable, but in any case a syntactically correctly formed proposition.

In contrast, in most flavors of type theory, the typing judgment X : Y is never a mathematically interesting question. Instead, the typing judgment is decidableβ€”indeed, verifying well-typedness is what Agda’s kernel is all about. Either X is mechanically known to be of type Y, or it has some other type (or is just ill-typed).

_∈_ : V β†’ V β†’ Set
x ∈ y = βˆƒ[ i ] (fam y i β‰ˆ x)
-- "x is an element of sup f iff it is equivalent to one of the
-- children of sup f."

cong-∈ : {x y z : V} β†’ x β‰ˆ y β†’ z ∈ x β†’ z ∈ y
cong-∈ = {!!}

cong-∈' : {x y z : V} β†’ x β‰ˆ y β†’ x ∈ z β†’ y ∈ z
cong-∈' = {!!}

As a basic sanity check, every child f i is an element of sup f; the following is a convenience function for some of the proofs below.

∈-basic : {x : V} β†’ (i : Index x) β†’ fam x i ∈ x
∈-basic = {!!}

Axiom of extensionality

infix 4 _↔_
_↔_ : {β„“ β„“' : Level} β†’ Set β„“ β†’ Set β„“' β†’ Set (β„“ βŠ” β„“')
A ↔ B = (A β†’ B) Γ— (B β†’ A)

A basic principle in set theory is that sets are determined by their elements: Two sets are equal if and only if they have the same elements. Our sets-as-trees model of set theory validates this principle (if we replace strict equality by _β‰ˆ_).

extensionality₁ : {x y : V} β†’ ((z : V) β†’ z ∈ x ↔ z ∈ y) β†’ x β‰ˆ y
extensionality₁ = {!!}

extensionalityβ‚‚ : {x y : V} β†’ x β‰ˆ y β†’ ((z : V) β†’ z ∈ x ↔ z ∈ y)
extensionalityβ‚‚ = {!!}

Basic set construction axioms

existence-empty-set : βˆƒ[ x ] ((y : V) β†’ y ∈ x β†’ βŠ₯)
existence-empty-set = {!!}

pairing-axiom : (x y : V) β†’ βˆƒ[ z ] (x ∈ z Γ— y ∈ z)
pairing-axiom = {!!}

union : V β†’ V
union = {!!}

union-axiom : (x : V) β†’ βˆƒ[ y ] ((z : V) β†’ z ∈ y ↔ βˆƒ[ w ] (z ∈ w Γ— w ∈ x))
union-axiom x = ?
-- TODO: Format as exercise

In the vincinity of Russell’s paradox

no-set-contains-itself : (v : V) β†’ v ∈ v β†’ βŠ₯
no-set-contains-itself = {!!}

It is tempting to introduce a set u of all sets, as follows:

u : V
u = sup {V} (Ξ» x β†’ x)

However, this attempt is rejected by Agda with the comment β€œSet₁ != Set when checking that the expression V has type Set”. The children of a node need to be indexed by a small type, a type in Set; but V itself is not a small type, but rather a type in Set₁.

Agda supports the unsafe option --type-in-type, collapsing the universe hierarchy. The definition of u is then well-typed, and a contradiction can be derived as follows.

u∈u : u ∈ u
u∈u = u , β‰ˆ-refl

contradiction : βŠ₯
contradiction = no-set-contains-itself u u∈u

Make this explorable in a submodule