Finn Lawler empty 7 (Rev #4, changes)

Showing changes from revision #3 to #4: 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,X, Y, \ldots of sorts, together with function symbols f:XYf \colon \vec X \to Y and relation symbols RXR \subset \vec X, where X\vec X is a finite list X 1,X 2,,X nX_1, X_2, \ldots, X_n of sorts, also called a type. We’ll denote types by X,Y,X,Y,\ldots too.

For each sort XX there should be an inexhaustible supply of fresh variables xx and bound variables ξ\xi of sort XX. A context is a finite list x:X\vec x \colon \vec X of sorted variables, or equivalently a single typed variable x:X 1,X 2,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)f(t) where ff is a function symbol and tt 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]t[x] to indicate that xx is the context of tt, and t[s]t[s] to denote the obvious substitution. The type of a term-in-context is determined in the obvious way: for variables, x i[x:X]:X ix_i[\vec x \colon \vec X] \colon X_i, while a tuple (t 1,t 2,,t n)[x:X]:XY(t_1, t_2, \ldots, t_n)[x \colon X] \colon X \to \vec Y if each t i:XY it_i \colon X \to Y_i, and f(t):XYf(t) \colon X \to Y if f:ZYf \colon Z \to Y and t:XZt \colon X \to Z.

Formulas

The formulas of regular logic are built up from the atomic formulas R(t)R(t) (where the type of tt is the type of RR) and t= Xst =_X s (where tt and ss are terms of type XX) using \top (true), \wedge (conjunction) and \exists, where if ϕ[x]\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 ϕ[t]\phi[t] of the term tt for the variable xx 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

ϕ[t]ξ.ϕ[ξ]ξ.ϕ[ξ]ϕ[x] ψψ \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 xx is not free in ψ\psi, and equality by

t=tt=sϕ[t]ϕ[s] \frac{}{t=t} \qquad \qquad \frac{t=s \qquad \phi[t]}{\phi[s]}

We also have to add the Frobenius axiom ϕy.ψy.(ϕψ)\phi \wedge \exists y. \psi \vdash \exists y.(\phi \wedge \psi), where yy is not in x\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:EBp \colon E \to B is a regular fibration, then an interpretation II of a signature assigns

  • to each sort XX an object IXI X of BB

  • to each list X=X 1,X 2,,X n\vec X = X_1, X_2, \ldots, X_n of sorts the product IX=IX 1×IX 2××IX nI \vec X = I X_1 \times I X_2 \times \cdots \times I X_n

  • to each function symbol f:XYf \colon \vec X \to Y a morphism If:IXIYI f \colon I \vec X \to I Y in BB

  • to each relation symbol RXR \subset \vec X an object IRI R in E IXE_{I \vec X} (the fibre of pp over IXI \vec X)

Given an interpretation of a signature, terms and formulas over it are given the following meanings:

  • I(x i[x])=π i:Π jX jX iI (x_i[\vec x]) = \pi_i \colon \Pi_j X_j \to X_i.

  • If(t 1,t 2,,t n)=If(It 1,It 2,,It n)I f(t_1, t_2, \ldots, t_n) = I f \circ (I t_1, I t_2, \ldots, I t_n).

  • IR(t 1,t 2,,t n)=(It i) i *IRI R(t_1, t_2, \ldots, t_n) = (I t_i)_i^* I R, where (It i) i(I t_i)_i is the pairing of the meanings of the t it_i.

  • I(x= Xx)= Δ IXI(x =_{\vec X} x') = \exists_{\Delta_{I \vec X}} \top, where Δ IX:IXIX×IX\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 EE, of course, and \exists by the left adjoints π\exists_\pi to product projections π\pi.

An interpretation II satisfies a sequent S=ϕ xψS = \phi \vdash_{\vec x} \psi, written ISI \models S, if there is a vertical morphism IϕIψI \phi \to I \psi over IXI \vec X where X\vec X is the sort of x\vec x.

An interpretation is a model of a theory, written ITI \models T, if it satisfies each sequent contained in the theory.

In the notes referenced above, we see that a regular theory TT gives rise to a syntactic model, a regular fibration E TB TE_T \to B_T. A model of TT in pp is then a morphism of regular fibrations from E TE_T to pp. The following then hold:

Soundness Theorem

If a theory TT proves a sequent SS, then for any model II of TT, ISI \models S.

Proof

TST \vdash S iff E TSE_T \models S, and morphisms of regular fibrations preserve entailment.

Completeness theorem

If every model of a theory TT models a sequent SS, then E TE_T models SS.

Proof

Trivial.

Revision on November 22, 2012 at 22:04:16 by Finn Lawler?. See the history of this page for a list of all contributions to it.