[[!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 type and a layer for propositions. We have the basic judgement forms of the type layer: * $\Gamma \vdash A\; \mathrm{type}$ - $A$ is a well-typed type in context $\Gamma$. * $\Gamma \vdash a:A$ - $a$ is a well-typed element of type $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 p::\phi \; \mathrm{true}$ - $p$ is a well-formed proof that $\phi$ is a 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{type}}{(\Gamma, a:A) \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash \phi \; \mathrm{prop}}{(\Gamma, p::\phi) \; \mathrm{ctx}}$$ ### 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