# Contents * contents {:toc} We'll roughly follow the [[nlab:Elephant]] and [Seely](References#seely83hyper). The following is all entirely standard and here only to fix notation and terminology. ## Type theory A **signature** is a collection $X, Y, \ldots$ of **types**, together with **function symbols** $f \colon \vec X \to Y$ and **relation symbols** $R \subset \vec X$, where $\vec X$ is a finite list $X_1, X_2, \ldots, X_n$ of types. For each sort $X$ there should be an inexhaustible supply of fresh variables of sort $X$. A **context** is a finite list $\vec x$ of variables, and the sort of a context is the list $\vec X$ of the sorts of the variables in it. A **term** of sort $X$ is either a variable of $x$ of sort $X$ or an expression of the form $f(t_1, t_2, \ldots, t_n)$ where $f \colon Y_1, Y_2, \ldots, Y_n \to X$ and each $t_i$ is a term of sort $Y_i$. The free variables of a term are precisely the variables that appear in it. ### Formulas The **formulas** of regular logic are built up from the atomic formulas $R(\vec t)$ (where the sort of $\vec t$ is the sort of $R$) and $t =_X s$ (where $t$ and $s$ are terms of sort $X$) using $\top$ (true), $\wedge$ (conjunction) and $\exists$. The **free variables** of a formula are defined in the usual way. A context $\vec x$ is **suitable** for a formula $\phi$ (term $t$) if the free variables of $\phi$ ($t$) are contained in $\vec x$. A formula $\phi$ (term $t$) taken in some suitable context $\vec x$ will be written $\phi[\vec x]$ ($t[\vec x]$), and $\phi$ by itself will often mean $\phi[FV(\phi)]$, with the free variables $FV(\phi)$ in some canonical order. The **substitution** $\phi[\vec t / \vec x]$ of the terms $\vec t$ for the variables $\vec x$ is defined as usual, as is the substitution $t[\vec s / \vec x]$. ## Logic A **sequent** (wrt a given signature) is an expression $\phi \vdash_{\vec x} \psi$ where the context $\vec x$ is suitable for both $\phi$ and $\psi$. A **theory** is a set of sequents (over the same signature, obviously). The **inference rules** of regular logic are the usual ones, including these $$ \frac{}{\phi \vdash_{\vec x} \phi} \text{(Axiom)} \qquad\qquad \frac{\phi \vdash_{\vec x} \psi \qquad \psi \vdash_{\vec x} \chi}{\phi \vdash_{\vec x} \chi} \text{(Cut)} $$ $$ \frac{\phi \vdash_{\vec x} \psi}{\phi[\vec t/ \vec x] \vdash_{\vec y} \psi[\vec t / \vec x]} \text{(Substitution)} $$ where $\vec y$ contains the variables of the terms $\vec t$. The other rules are as in [Seely](References#seely83hyper). We also have to add the **Frobenius axiom** $\phi \wedge \exists y. \psi \vdash_{\vec x} \exists y.(\phi \wedge \psi)$, where $y$ is not in $\vec x$. Proofs are considered up to the rewrites given in [Seely](References#seely83hyper) and [Prawitz](References#prawitz65natded), together with those making the Frobenius axiom the two-sided inverse to the usual proof of the converse (see e.g. [Elephant p. 832](References#elephant)). ## Models Models of regular theories are [[regular fibrations]]. If $p \colon E \to B$ is a regular fibration, then an **interpretation** $I$ of a signature assigns * to each sort $X$ an object $I X$ of $B$ * to each list $\vec X = X_1, X_2, \ldots, X_n$ of sorts the product $I \vec X = I X_1 \times I X_2 \times \cdots \times I X_n$ * to each function symbol $f \colon \vec X \to Y$ a morphism $I f \colon I \vec X \to I Y$ in $B$ * to each relation symbol $R \subset \vec X$ an object $I R$ in $E_{I \vec X}$ (the fibre of $p$ over $I \vec X$) Given an interpretation of a signature, terms and formulas over it are given the following meanings: * $I (x_i[\vec x]) = \pi_i \colon \Pi_j X_j \to X_i$. * $I f(t_1, t_2, \ldots, t_n) = I f \circ (I t_1, I t_2, \ldots, I t_n)$. * $I R(t_1, t_2, \ldots, t_n) = (I t_i)_i^* I R$, where $(I t_i)_i$ is the pairing of the meanings of the $t_i$. * $I(x =_{\vec X} x') = \exists_{\Delta_{I \vec X}} \top$, where $\Delta_{I \vec X} \colon I \vec X \to I \vec X \times I \vec X$ is the diagonal. * $\top$ and $\wedge$ are interpreted by the finite products in $E$, of course, and $\exists$ by the left adjoints $\exists_\pi$ to product projections $\pi$. An interpretation $I$ **satisfies** a sequent $S = \phi \vdash_{\vec x} \psi$, written $I \models S$, if there is a vertical morphism $I \phi \to I \psi$ over $I \vec X$ where $\vec X$ is the sort of $\vec x$. An interpretation is a **model** of a theory, written $I \models T$, if it satisfies each sequent contained in the theory. +-- {: .un_prop } ###### Soundness Theorem If a theory $T$ proves a sequent $S$, then for any model $I$ of $T$, $I \models S$. =-- +-- {: .proof } ###### Proof ... =--