[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Forget about real analysis. If we are already using Archimedean ordered Artinian local $R$-algebras, we could continue and use the complexification $C = R[i]/(i^2 + 1)$ of the Archimedean ordered field $R$ instead. Synthetic complex analysis to define the complex exponential function on $C$, and the complex sine and cosine function straight into trigonometry. ## Presentation ### Judgments and contexts Set theory is a type theory which consists of two layers, a layer for sets and a layer for propositions. We have the basic judgement forms of the set layer: * $\Gamma \vdash A\; \mathrm{set}$ - $A$ is a well-typed set in context $\Gamma$. * $\Gamma \vdash a \in A$ - $a$ is a well-typed element of set $A$ in context $\Gamma$. And the basic judgement forms of the proposition layer: * $\Gamma \vdash \phi \; \mathrm{prop}$ - $\phi$ is a well-formed proposition in context $\Gamma$ * $\Gamma \vdash \phi \; \mathrm{true}$ - $\phi$ is a well-formed true proposition in context $\Gamma$ As well as context judgments: * $\Gamma \; \mathrm{ctx}$ - $\Gamma$ is a well-formed context. Contexts are defined by the following rules: $$\frac{}{() \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash A \; \mathrm{set}}{(\Gamma, a \in A) \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash \phi \; \mathrm{prop}}{(\Gamma, \phi \; \mathrm{true}) \; \mathrm{ctx}}$$ ### Structural rules There are three structural rules in set theory, the variable rules, the [[weakening rules]], and the [[substitution rule]]. The variable rules states that we may derive a membership judgment or a true proposition judgment if the membership judgment or true proposition judgment is in the context already: $$\frac{\Gamma, a \in A, \Delta \; \mathrm{ctx}}{\Gamma, a \in A, \Delta \vdash a \in A} \qquad \frac{\Gamma, P \; \mathrm{true}, \Delta \; \mathrm{ctx}}{\Gamma, P \; \mathrm{true}, \Delta \vdash P \; \mathrm{true}}$$ Let $\mathcal{J}$ be any arbitrary judgment. Then we have the following rules: The weakening rule: $$\frac{\Gamma, \Delta \vdash \mathcal{J} \quad \Gamma \vdash A \; \mathrm{type}}{\Gamma, a \in A, \Delta \vdash \mathcal{J}} \qquad \frac{\Gamma, \Delta \vdash \mathcal{J} \quad \Gamma \vdash P \; \mathrm{prop}}{\Gamma, P \; \mathrm{true}, \Delta \vdash \mathcal{J}}$$ The substitution rule: $$\frac{\Gamma \vdash a \in A \quad \Gamma, b \in A, \Delta\vdash \mathcal{J}}{\Gamma, \Delta[a/b] \vdash \mathcal{J}[a/b]}$$ The weakening and substitution rules are admissible rules: they do not need to be explicitly included in the type theory as they could be proven by induction on the structure of all possible derivations. ### Bounded universal quantifier Formation rules for the bounded universal quantifier: $$\frac{\Gamma \vdash A \; \mathrm{set} \quad \Gamma, x \in A \vdash P \; \mathrm{prop}}{\Gamma \vdash \forall x \in A.P(x) \; \mathrm{prop}}$$ Introduction rules for the bounded universal quantifier: $$\frac{\Gamma \vdash A \; \mathrm{set} \quad \Gamma, x:A \vdash P \; \mathrm{prop} \quad \Gamma, x:A \vdash P \; \mathrm{true}}{\Gamma \vdash \forall x \in A.P(x) \; \mathrm{true}}$$ Elimination rules for the bounded universal quantifier: $$\frac{\Gamma \vdash A \; \mathrm{set} \quad \Gamma, x \in A \vdash P \; \mathrm{prop} \quad \Gamma \vdash \forall x \in A.B(x) \; \mathrm{true}}{\Gamma, x \in A \vdash P \; \mathrm{true}}$$ ### Separation A predicate on a set $A$ is a proposition $x \in A \vdash P \; \mathrm{prop}$. Bounded separation states that given a predicate $P$ on a set $A$, one could construct the set $\vert P \vert$ with an injection $i:\vert P \vert \hookrightarrow A$ $$\frac{\Gamma \vdash A \; \mathrm{set} \quad \Gamma, x \in A \vdash P \; \mathrm{prop}}{\Gamma \vdash \vert P \vert \; \mathrm{set}}$$ $$\frac{\Gamma \vdash A \; \mathrm{set} \quad \Gamma, x \in A \vdash P \; \mathrm{prop}}{\Gamma \vdash i:\vert P \vert \to A}$$ $$\frac{\Gamma \vdash A \; \mathrm{set} \quad \Gamma, x \in A \vdash P \; \mathrm{prop}}{\Gamma, x \in A, y \in A \vdash (x = y) \iff i(x) = i(y) \; \mathrm{true}}$$ $$\frac{\Gamma \vdash A \; \mathrm{set} \quad \Gamma, x \in A \vdash P \; \mathrm{prop}}{\Gamma, x \in A \vdash P(x) \iff \exists y:\vert P \vert.i(y) = x \; \mathrm{true}}$$ category: redirected to nlab