Class Theory NBG: the Axioms, Standing Conventions and Basic Notation

This setting bundles the axioms and basic notation of the class theory NBG; its logical framework is that of The Logical Framework of the Foundations: Classical First-Order Logic, the Informal Metatheory, and the Class Theory NBG.

1. (Objects)¶ The objects are classes, with membership $\in$; sets and proper classes are as defined there. Every element of a class is a set by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §elements.

2. (Axioms) The following axioms are in force: ¶ extensionality, Axiom of Extensionality for Classes; ¶ pairing, Axiom of Pairing; ¶ the empty set, Axiom of the Empty Set; ¶ class existence, Axioms of Class Existence (Gödel's Axioms B1-B7); ¶ separation, Axiom of Separation for Classes; ¶ union, Axiom of Union; ¶ power set, Axiom of Power Set; ¶ replacement, Axiom of Replacement for Classes; ¶ infinity, Axiom of Infinity; ¶ foundation, Axiom of Foundation for Classes.

3. (Comprehension)¶ Classes are formed by class abstraction $\{x:\varphi\}$ and $\{x\in A:\varphi\}$ for predicative formulas $\varphi$, possibly written with abbreviations, as justified by The Class Comprehension Theorem for Predicative Formulas §comprehension.

4. (Notation)¶ $\emptyset$, $\{x,y\}$ and $\{x\}$ are as in The Empty Set, the Unordered Pair and the Singleton §empty, The Empty Set, the Unordered Pair and the Singleton §pair and The Empty Set, the Unordered Pair and the Singleton §singleton; $(x,y)$ as in The Ordered Pair of Two Sets and Nested Tuples §pair and $\langle x_{1},\dots,x_{n}\rangle$ as in The Ordered Pair of Two Sets and Nested Tuples §tuple; $\subseteq$ as in Subclasses and Subsets §subclass; $\cap$, $\cup$ and $\setminus$ as in The Boolean Operations on Classes, Disjointness, and the Universal Class §operations, and $V$ as in The Boolean Operations on Classes, Disjointness, and the Universal Class §universe; $\bigcup x$ as in The Union Set and the Power Set of a Set §union and $\mathcal{P}(x)$ as in The Union Set and the Power Set of a Set §power. Unless stated otherwise, in items adopting this setting lower-case letters denote sets and upper-case letters denote classes; parameters of class abstractions may be of either kind, as Class Abstraction: the Class of All Sets Satisfying a Predicative Formula allows.

5. (Background)¶ The following results are in force by reference: Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique, The Characteristic Property of Ordered Pairs and Nested Tuples of Sets and Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper.