Showing changes from revision #2 to #3: Added | Removed | Changed

Contents

We’ll roughly follow the Elephant and Seely. The following is all entirely standard and here only to fix notation and terminology.

For more details, see these notes.

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. A context.

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

existentials by

where on the right $x$ is not free in $\psi$, and equality by

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 and Prawitz, together with those making the Frobenius axiom the two-sided inverse to the usual proof of the converse (see e.g. Elephant p. 832 ). 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.

Soundness Theorem

If a theory $T$ proves a sequent $S$, then for any model $I$ of $T$, $I \models S$.

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:

Proof

$T \vdash S$ iff $E_T \models S$, and morphisms of regular fibrations preserve entailment.

Completeness theorem

If every model of a theory $T$ models a sequent $S$, then $E_T$ models $S$.

Trivial.