Showing changes from revision #1 to #2: 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 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 types. sorts, also called atype. We’ll denote types by $X,Y,\ldots$ too.

For each sort $X$ there should be an inexhaustible supply of fresh variables of sort$\mathrm{<span><del\; class="diffmod">\; X</del><ins\; class="diffmod">\; x</ins></span>}$ X x . A and bound variables$\xi$ of sort $X$. A context is a finite list $\overrightarrow{x}:\overrightarrow{X}$ \vec x \colon \vec X of sorted variables, and or the equivalently sort of a context single is typed the variable list$\overrightarrow{X}x:X_1,X_2,\dots$ \vec x X \colon X_1, X_2, \ldots . of the sorts of the variables in it.

A term is either a variable, a tuple of sort terms, or an expression of the form$\mathrm{<span><del\; class="diffmod">\; X</del><ins\; class="diffmod">\; f</ins></span>}(t)$ X f(t) is where either a variable of$\mathrm{<span><del\; class="diffmod">\; x</del><ins\; class="diffmod">\; f</ins></span>}$ x f of is sort a function symbol and$\mathrm{<span><del\; class="diffmod">\; X</del><ins\; class="diffmod">\; t</ins></span>}$ X t or a an term. expression The free variables of a term are precisely the form 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$\mathrm{<span><del\; class="diffmod">\; f</del><ins\; class="diffmod">\; t</ins></span>}<span><del\; class="diffmod">\; (</del><ins\; class="diffmod">\; [</ins></span>t_{1}x<span><del\; class="diffmod">\; ,</del><ins\; class="diffmod">\; ]</ins></span>t_2,\dots ,t_n)$ f(t_1, t[x] t_2, \ldots, t_n) where to indicate that$\mathrm{<span><del\; class="diffmod">\; f</del><ins\; class="diffmod">\; x</ins></span>}:Y_1,Y_2,\dots ,Y_n\to X$ f x \colon Y_1, Y_2, \ldots, Y_n \to X and is each the context of$t_{i}t$ t_i t , is and a term of sort$Y_{i}t[s]$ Y_i t[s] . to denote the obvious substitution. The free type variables of a term term-in-context are is precisely determined the variables that appear in it. 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(\overrightarrow{t}t)$ R(\vec R(t) t) (where the sort type of$\overrightarrow{t}t$ \vec t is the sort type of$R$) and $t =_X s$ (where $t$ and $s$ are terms of sort type$X$) using $\top$ (true), $\wedge$ (conjunction) and $\exists$ . , The 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 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 $\varphi [\overrightarrow{t}t/\overrightarrow{x}]$ \phi[\vec \phi[t] t / \vec x] of the terms term$\overrightarrow{t}t$ \vec t for the variables variable$\overrightarrow{x}x$ \vec x is defined as usual, usual. as is the substitution$t[\vec s / \vec x]$.

Logic

A We’ll use the usual natural-deduction rules — conjunction and truth are governed bysequent (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).