Theory of proveit.logic.classes

A class is a collection of sets. Its members are defined by a shared property. A class need not be a set with a well-defined ordinal rank (for example, the class of ordinals cannot have a ordinal rank and must not be a set if we are to avoid the Burali-Forti paradox).

import proveit
%theory # toggles between interactive and static modes

Local content of this theory

common expressions	axioms	theorems	demonstrations

Sub-theories

membership

All axioms contained within this theory

This theory contains no axioms directly.

proveit.logic.classes.membership

proveit.logic.classes.membership.not_in_class_def