Spahn
rules of type theories (Rev #2, changes)

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

  • Bart jacobs, Categorical logic and type theory

p.121-123 lists the followings following as the basic rules of simple type theory:

(1) identity

x:Xx:X\frac{}{x:X\vdash x:X}

(2) function symbol

M 1: x s 1M n: x s nF(M 1,,M n: x s n+1) \frac{M_1:x_1\;\;\dots \frac{M_1:s_1\;\;\dots \;\; M_n:x_n}{F(M_1,\dots,M_n:x_{n+1}} M_n:s_n}{F(M_1,\dots,M_n:s_{n+1})}

for F: x s 1,, x s n x s n+1 F:x_1,\dots,x_n\to F:s_1,\dots,s_n\to x_{n+1} s_{n+1} in Σ\Sigma

(3) weakening

x 1:s 1,x n:s nM:tx 1:s 1,,x n:s n,x n+1,s n+1M:t\frac{x_1:s_1,\;\dots\;x_n:s_n\vdash M:t}{x_1:s_1,\dots,x_n:s_n,x_{n+1},s_{n+1}\vdash M:t}

(4) contraction

Γ,x n:s,x n+1:sM:tΓ,x n:sM[x n/x n+1]:t\frac{\Gamma, x_n: s, x_{n+1}: s\vdash M:t}{\Gamma, x_n: s\vdash M[x_n / x_{n+1}]: t}

(5) exchange

where we omitted the Γ\Gamma \vdash which we could prefix to every typing judgement.

Γ,x i:s i,x i+1:s i+1,ΔM:tΓ,x i:s i+1,x i+1:s i,ΔM[x i/x it1,x i+1/x i]:t\frac{\Gamma, x_i:s_i, x_{i+1}:s_{i+1},\Delta\vdash M: t}{\Gamma, x_i:s_{i+1}, x_{i+1}: s_i,\Delta\vdash M[x_i/x_{it1},x_{i+1}/x_i]:t}

where we omitted (except in (4) and (5)) the Γ\Gamma \vdash which we could prefix to every typing judgement.

From these rule one can derive a further important rule:

(6) substitution

x n:sM:tN:sM[N/x n]:t\frac{x_n:s\vdash M:t\;\;\; N:s}{M[N/x_n]:t}

Revision on February 26, 2013 at 02:53:29 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.