Showing changes from revision #0 to #1: 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.

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

where $\vec y$ contains the variables of the terms $\vec t$. The other rules are as in Seely. 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 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).

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.