Classes are syntax sugar for formulas 🔗

Author: Wisp

Intro 🔗

In classical set theory, we make a distinction between classes and sets. Every set is a class, but some classes are not sets. The classes which are not also sets are called "proper classes". Proper classes are similar to sets, but they are always very big.

Classes are defined using class-builder notation: { x | some formula }.

For example, { x | 0 < x and x < 10 } is the class of all natural numbers between 0 and 10 (assuming < is defined only on natural numbers). In this case, the class is also a set. On the other hand, the class { x | x = x } is a proper class, and contains everything.

So what exactly is a class? In ZFC, classes are syntax sugar on sets. There are three parts to this syntax sugar.

Membership in a Class 🔗

The statement x ∈ { y | some formula } can be reduced by replacing every occurence of y in some formula with x. For example, x ∈ { y | y < 10 } can be replaced by x < 10.

This replacement will always produce a formula which is true iff the original formula was true. In this way, we can eliminate membership in a class from the language.

Class Equality 🔗

Given two classes { x | some formula } and { y | some formula }, we say that they are equal iff they have the same members. So given the statement { x | x < 10 } = { y | y <= 9 }, we can transform it like into this:

∀z ( z ∈ { x | x < 10 } <-> z ∈ { y | y <= 9 } )

Which can then be reduced further, eliminating all classes from the statement:

∀z ( z < 10 <-> z <= 9 )

Class Membership 🔗

Given the formula { x | x < 10 } ∈ { y | y ⊆ ℕ }, we can reduce it by transforming the left-hand side into a set. We do so this way:

∃z ( z = { x | x < 10 } and z ∈ { y | y ⊆ ℕ } )

Which can then be reduced farther:

∃z ( ∀w ( w ∈ z <-> w < 10 ) and z ∈ { y | y ⊆ ℕ } )

∃z ( ∀w ( w ∈ z <-> w < 10 ) and z ⊆ ℕ )

And then we are done, all classes have been eliminated.

Meta 🔗

Home Page

Date: 2022-10-21