# 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. For more details, see [[reglog.pdf|these notes:file]]. ## Type theory A **signature** is a collection $X, Y, \ldots$ of **sorts**, 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 sorts, also called a **type**. We'll denote types by $X,Y,\ldots$ too. For each sort $X$ there should be an inexhaustible supply of fresh variables $x$ and bound variables $\xi$ of sort $X$. A **context** is a finite list $\vec x \colon \vec X$ of sorted variables, or equivalently a single typed variable $x \colon X_1, X_2, \ldots$. A **term** is either a variable, a tuple of terms, or an expression of the form $f(t)$ where $f$ is a function symbol and $t$ a term. The free variables of a term are precisely the variables that appear in it. Each term lives in a context, which must contain every variable in the term, perhaps together with 'dummy' variables that don't. We write $t[x]$ to indicate that $x$ is the context of $t$, and $t[s]$ to denote the obvious substitution. The type of a term-in-context is determined in the obvious way: for variables, $x_i[\vec x \colon \vec X] \colon X_i$, while a tuple $(t_1, t_2, \ldots, t_n)[x \colon X] \colon X \to \vec Y$ if each $t_i \colon X \to Y_i$, and $f(t) \colon X \to Y$ if $f \colon Z \to Y$ and $t \colon X \to Z$. ### Formulas The **formulas** of regular logic are built up from the atomic formulas $R(t)$ (where the type of $t$ is the type of $R$) and $t =_X s$ (where $t$ and $s$ are terms of type $X$) using $\top$ (true), $\wedge$ (conjunction) and $\exists$, where if $\phi[x]$ is a formula then so is $\exists \xi.\phi[\xi]$. The **free variables** of a formula are defined in the usual way. The **substitution** $\phi[t]$ of the term $t$ for the variable $x$ is defined as usual. ## Logic We'll use the usual natural-deduction rules --- conjunction and truth are governed by $$ \frac{\phi \qquad \psi}{\phi \wedge \psi} \qquad \qquad \frac{\phi \wedge \psi}{\phi} \qquad \frac{\phi \wedge \psi}{\psi} \qquad \qquad \frac{\phi}{\top} $$ existentials by $$ \frac{\phi[t]}{\exists \xi.\phi[\xi]} \qquad \qquad \frac{ \exists \xi.\phi[\xi] \qquad \begin{array}[b]{c} \phi[x] \\ \vdots \\ \psi \end{array} } {\psi} $$ where on the right $x$ is not free in $\psi$, and equality by $$ \frac{}{t=t} \qquad \qquad \frac{t=s \qquad \phi[t]}{\phi[s]} $$ We also have to add the **Frobenius axiom** $\phi \wedge \exists y. \psi \vdash \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)). Again, see the notes referenced above. ## 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. In the notes referenced above, we see that a regular theory $T$ gives rise to a syntactic model, a regular fibration $E_T \to B_T$. A model of $T$ in $p$ is then a morphism of regular fibrations from $E_T$ to $p$. The following then hold: +-- {: .un_theorem } ###### Soundness Theorem If a theory $T$ proves a sequent $S$, then for any model $I$ of $T$, $I \models S$. =-- +-- {: .proof } ###### Proof $T \vdash S$ iff $E_T \models S$, and morphisms of regular fibrations preserve entailment. =-- +-- {: .un_theorem } ###### Completeness theorem If every model of a theory $T$ models a sequent $S$, then $E_T$ models $S$. =-- +-- {: .proof } ###### Proof Trivial. =--