[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Type theory (dependent function types, dependent sum types, identity types, function extensionality) -> Predicate logic -> Set theory -> Number theory Russell universes are formally defined in a three-layer type theory. The first and second layers consists of an untyped [[predicate logic]] consisting of proposition judgments and index judgments, the [[natural deduction]] rules for [[predicate logic]], and inference rules to define a [[linear order]] without an [[upper bound]], or more commonly, the inference rules for [[first-order theory|first-order]] [[Peano arithmetic]]. The third layer only contains term judgments, and is the dependent type theory where the Russell universes live in. We begin with the formal rules of the first and second layers. The first and second layer consists of three judgments: proposition judgments $A \; \mathrm{prop}$, where we judge $A$ to be a proposition, true proposition judgments $A \; \mathrm{true}$, where we judge $A$ to be a true proposition, index judgments, where we judge $a$ to be a universe index, $a \; \mathrm{index}$, and metacontext judgments, where we judge $\Xi$ to be a metacontext, $\Xi \; \mathrm{metactx}$. Metacontexts are lists of index judgments $a \; \mathrm{index}$, $b \; \mathrm{index}$, $c \; \mathrm{index}$, et cetera, and true proposition judgments $A \; \mathrm{true}$, $B \; \mathrm{true}$, $C \; \mathrm{true}$, et cetera, and are formalized by the rules for the empty metacontext and extending the metacontext by an index judgment or true proposition judgment: $$\frac{}{() \; \mathrm{metactx}} \qquad \frac{\Xi \; \mathrm{metactx} \quad \Xi \vdash A \; \mathrm{prop}}{(\Xi, A \; \mathrm{true}) \; \mathrm{metactx}} \qquad \frac{\Xi \; \mathrm{metactx}}{(\Xi, i \; \mathrm{index}) \; \mathrm{metactx}}$$ Next, we have the inference rules for [[propositional logic]]: * Rules for false: $$\frac{\Xi \; \mathrm{metactx}}{\Xi \vdash \bot \; \mathrm{prop}} \qquad \frac{\Xi \vdash P \; \mathrm{prop}}{\Xi, \bot \; \mathrm{true} \vdash P \; \mathrm{true}}$$ * Rules for negation: $$\frac{\Xi \vdash P \; \mathrm{prop}}{\Xi \vdash \neg P \; \mathrm{prop}} \qquad \frac{\Xi \vdash P \; \mathrm{prop} \quad \Xi, P \; \mathrm{true} \vdash \bot \; \mathrm{true}}{\Xi \vdash \neg P \; \mathrm{true}} \qquad \frac{\Xi \vdash \neg P \; \mathrm{true}}{\Xi, P \; \mathrm{true} \vdash \bot \; \mathrm{true}}$$ * Rules for implication: $$\frac{\Xi \vdash P \; \mathrm{prop} \quad \Xi \vdash Q \; \mathrm{prop}}{\Xi \vdash P \to Q \; \mathrm{prop}} \qquad \frac{\Xi \vdash P \; \mathrm{prop} \quad \Xi, P \; \mathrm{true} \vdash Q \; \mathrm{true}}{\Xi \vdash P \to Q \; \mathrm{true}} \qquad \frac{\Xi \vdash P \to Q \; \mathrm{true}}{\Xi, P \; \mathrm{true} \vdash Q \; \mathrm{true}}$$ * Rules for conjunction: $$\frac{\Xi \vdash P \; \mathrm{prop} \quad \Xi \vdash Q \; \mathrm{prop}}{\Xi \vdash P \wedge Q \; \mathrm{prop}} \quad \frac{\Xi \vdash P \; \mathrm{true} \quad \Xi \vdash Q \; \mathrm{true}}{\Xi \vdash P \wedge Q \; \mathrm{true}}$$ $$\frac{\Xi \vdash P \; \mathrm{prop} \quad \Xi \vdash Q \; \mathrm{prop} \quad \Xi, P \wedge Q \; \mathrm{true}}{\Xi \vdash P \; \mathrm{true}} \qquad \frac{\Xi \vdash P \; \mathrm{prop} \quad \Xi \vdash Q \; \mathrm{prop} \quad \Xi, P \wedge Q \; \mathrm{true}}{\Xi \vdash Q \; \mathrm{true}}$$ * Rules for disjunction: $$\frac{\Xi \vdash P \; \mathrm{prop} \quad \Xi \vdash Q \; \mathrm{prop}}{\Xi \vdash P \vee Q \; \mathrm{prop}} \qquad \frac{\Xi \vdash P \; \mathrm{prop} \quad \Xi \vdash Q \; \mathrm{prop}}{\Xi, P \; \mathrm{true} \vdash P \vee Q \; \mathrm{true}} \qquad \frac{\Xi \vdash P \; \mathrm{prop} \quad \Xi \vdash Q \; \mathrm{prop}}{\Xi, Q \; \mathrm{true} \vdash P \vee Q \; \mathrm{true}}$$ $$\frac{\Xi \vdash P \; \mathrm{prop} \quad \Xi \vdash Q \; \mathrm{prop} \quad \Xi, P \vee Q \; \mathrm{true} \vdash R \; \mathrm{prop} \quad \Xi, P \; \mathrm{true} \vdash R \; \mathrm{true} \quad \Xi, Q \; \mathrm{true} \vdash R \; \mathrm{true}}{\Xi, P \vee Q \; \mathrm{true} \vdash R \; \mathrm{true}}$$ Finally, we have the [[inference rules]] for a [[strict order]] which has no [[upper bound]]: $$\frac{\Xi \vdash x \; \mathrm{index} \quad \Xi \vdash y \; \mathrm{index}}{\Gamma \vdash x \lt y \; \mathrm{prop}} \quad \frac{\Xi \vdash x \; \mathrm{index}}{\neg (x \lt x) \; \mathrm{true}}$$ $$\frac{\Xi \vdash x \; \mathrm{index} \quad \Xi \vdash y \; \mathrm{index}}{\Gamma \vdash \neg ((x \lt y) \wedge (y \lt x)) \; \mathrm{true}}$$ $$\frac{\Xi \vdash x \; \mathrm{index} \quad \Xi \vdash y \; \mathrm{index} \quad \Xi \vdash z \; \mathrm{index}}{\Gamma \vdash (x \lt z) \implies ((x \lt y) \vee (y \lt z)) \; \mathrm{true}}$$ $$\frac{\Xi \vdash x \; \mathrm{index} \quad \Xi \vdash y \; \mathrm{index}}{x = y \; \mathrm{prop}} \qquad \frac{\Xi \vdash x \; \mathrm{index} \quad \Xi \vdash y \; \mathrm{index}}{(\neg (x \lt y)) \wedge (\neg (y \lt x)) \iff (x = y) \; \mathrm{true}}$$ $$\frac{\Xi \vdash x \mathrm{index}}{\Gamma \vdash s(x) \; \mathrm{index}} \qquad \frac{\Xi \vdash x \mathrm{index}}{\Gamma \vdash x \lt s(x) \; \mathrm{true}}$$ category: redirected to nlab