Martin Escardo 22-23 May 2013

GΓΆdel's system T and its standard set-theoretical semantics.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module EffectfulForcing.MFPSAndVariations.SystemT where

open import MLTT.Spartan  hiding (rec ; _^_) renaming (⋆ to 〈βŒͺ)
open import MLTT.Fin
open import EffectfulForcing.MFPSAndVariations.Combinators
open import EffectfulForcing.MFPSAndVariations.Continuity
open import UF.Base

data type : 𝓀₀ Μ‡ where
 ΞΉ   : type
 _β‡’_ : type β†’ type β†’ type

infixr 6 _β‡’_

\end{code}

We work with vector types which notational grow at the end rather than
the head.  This is because we use vector types to represent contexts,
which traditionally grow at the end:

\begin{code}

_^_ : 𝓀 Μ‡ β†’ β„• β†’ 𝓀 Μ‡
X ^ 0        = πŸ™
X ^ (succ n) = X ^ n Γ— X

infixr 3 _^_

_[_] : {X : Set} {n : β„•} β†’ X ^ n β†’ Fin n β†’ X
_[_] {X} {succ n} (xs , x) 𝟎       = x
_[_] {X} {succ n} (xs , x) (suc i) = xs [ i ]

Cxt : β„• β†’ 𝓀₀ Μ‡
Cxt n = type ^ n

data T : {n : β„•} (Ξ“ : Cxt n) (Οƒ : type) β†’ Type where
 Zero : {n : β„•} {Ξ“ : Cxt n} β†’ T Ξ“ ΞΉ
 Succ : {n : β„•} {Ξ“ : Cxt n} β†’ T Ξ“ (ΞΉ β‡’ ΞΉ)
 Rec  : {n : β„•} {Ξ“ : Cxt n} {Οƒ : type}   β†’ T Ξ“ ((ΞΉ β‡’ Οƒ β‡’ Οƒ) β‡’ Οƒ β‡’ ΞΉ β‡’ Οƒ)
 Ξ½    : {n : β„•} {Ξ“ : Cxt n} (i : Fin n)  β†’ T Ξ“ (Ξ“ [ i ])
 Ζ›    : {n : β„•} {Ξ“ : Cxt n} {Οƒ Ο„ : type} β†’ T (Ξ“ , Οƒ) Ο„ β†’ T Ξ“ (Οƒ β‡’ Ο„)
 _Β·_  : {n : β„•} {Ξ“ : Cxt n} {Οƒ Ο„ : type} β†’ T Ξ“ (Οƒ β‡’ Ο„) β†’ T Ξ“ Οƒ β†’ T Ξ“ Ο„

infixl 6 _Β·_

\end{code}

The standard interpretation of system T:

\begin{code}

γ€–_γ€— : type β†’ 𝓀₀ Μ‡
γ€– ΞΉ γ€—     = β„•
γ€– Οƒ β‡’ Ο„ γ€— = γ€– Οƒ γ€— β†’ γ€– Ο„ γ€—

【_】 : {n : β„•} (Ξ“ : Cxt n) β†’ 𝓀₀ Μ‡
【 Ξ“ 】 = (i : Fin _) β†’ γ€– Ξ“ [ i ] γ€—

⟨⟩ : 【 〈βŒͺ 】
⟨⟩ ()

_β€š_ : {n : β„•} {Ξ“ : Cxt n} {Οƒ : type} β†’ 【 Ξ“ 】 β†’ γ€– Οƒ γ€— β†’ 【 Ξ“ , Οƒ 】
(xs β€š x)  𝟎      = x
(xs β€š x) (suc i) = xs i

infixl 6 _β€š_

⟦_⟧ : {n : β„•} {Ξ“ : Cxt n} {Οƒ : type} β†’ T Ξ“ Οƒ β†’ 【 Ξ“ 】 β†’ γ€– Οƒ γ€—
⟦ Zero  ⟧  _ = 0
⟦ Succ  ⟧  _ = succ
⟦ Rec   ⟧  _ = rec
⟦ ν i   ⟧ xs = xs i
⟦ Ζ› t   ⟧ xs = Ξ» x β†’ ⟦ t ⟧ (xs β€š x)
⟦ t · u ⟧ xs = (⟦ t ⟧ xs) (⟦ u ⟧ xs)

\end{code}

Closed terms can be interpreted in a special way:

\begin{code}

Tβ‚€ : type β†’ Type
Tβ‚€ = T 〈βŒͺ

⟦_βŸ§β‚€  : {Οƒ : type} β†’ Tβ‚€ Οƒ β†’ γ€– Οƒ γ€—
⟦ t βŸ§β‚€ = ⟦ t ⟧ ⟨⟩

T-definable : {Οƒ : type} β†’ γ€– Οƒ γ€— β†’ Type
T-definable {Οƒ} x = Ξ£ t κž‰ Tβ‚€ Οƒ , ⟦ t βŸ§β‚€ ＝ x

\end{code}

System T extended with a formal oracle Ξ©, called T' (rather than TΞ© as previously):

\begin{code}

data T' : {n : β„•} (Ξ“ : Cxt n) (Οƒ : type) β†’ Type where
 Ξ©    : {n : β„•} {Ξ“ : Cxt n} β†’ T' Ξ“ (ΞΉ β‡’ ΞΉ)
 Zero : {n : β„•} {Ξ“ : Cxt n} β†’ T' Ξ“ ΞΉ
 Succ : {n : β„•} {Ξ“ : Cxt n} β†’ T' Ξ“ (ΞΉ β‡’ ΞΉ)
 Rec  : {n : β„•} {Ξ“ : Cxt n} β†’ {Οƒ : type}   β†’ T' Ξ“ ((ΞΉ β‡’ Οƒ β‡’ Οƒ) β‡’ Οƒ β‡’ ΞΉ β‡’ Οƒ)
 Ξ½    : {n : β„•} {Ξ“ : Cxt n} β†’ (i : Fin n)  β†’ T' Ξ“ (Ξ“ [ i ])
 Ζ›    : {n : β„•} {Ξ“ : Cxt n} β†’ {Οƒ Ο„ : type} β†’ T' (Ξ“ , Οƒ) Ο„ β†’ T' Ξ“ (Οƒ β‡’ Ο„)
 _Β·_  : {n : β„•} {Ξ“ : Cxt n} β†’ {Οƒ Ο„ : type} β†’ T' Ξ“ (Οƒ β‡’ Ο„) β†’ T' Ξ“ Οƒ β†’ T' Ξ“ Ο„


⟦_⟧' : {n : β„•} {Ξ“ : Cxt n} {Οƒ : type} β†’ T' Ξ“ Οƒ β†’ Baire β†’ 【 Ξ“ 】 β†’ γ€– Οƒ γ€—
⟦ Ω     ⟧' α  _ = α
⟦ Zero  ⟧' _  _ = 0
⟦ Succ  ⟧' _  _ = succ
⟦ Rec   ⟧' _  _ = rec
⟦ ν i   ⟧' _ xs = xs i
⟦ Ζ› t   ⟧' Ξ± xs = Ξ» x β†’ ⟦ t ⟧' Ξ± (xs β€š x)
⟦ t · u ⟧' α xs = (⟦ t ⟧' α xs) (⟦ u ⟧' α xs)

\end{code}

To regard system T as a sublanguage of T', we need to work with an
explicit embedding:

\begin{code}

embed : {n : β„•} {Ξ“ : Cxt n} {Οƒ : type} β†’ T Ξ“ Οƒ β†’ T' Ξ“ Οƒ
embed Zero    = Zero
embed Succ    = Succ
embed Rec     = Rec
embed (Ξ½ i)   = Ξ½ i
embed (Ζ› t)   = Ζ› (embed t)
embed (t Β· u) = (embed t) Β· (embed u)

preservation : {n : β„•}
               {Ξ“ : Cxt n}
               {Οƒ : type}
               (t : T Ξ“ Οƒ)
               (Ξ± : Baire)
             β†’ ⟦ t ⟧ ＝ ⟦ embed t ⟧' Ξ±
preservation Zero    Ξ± = refl
preservation Succ    Ξ± = refl
preservation Rec     Ξ± = refl
preservation (Ξ½ i)   Ξ± = refl
preservation (Ζ› t)   Ξ± = ap (Ξ» f xs x β†’ f (xs β€š x)) (preservation t Ξ±)
preservation (t Β· u) Ξ± = apβ‚‚ (Ξ» f g x β†’ f x (g x))
                             (preservation t Ξ±)
                             (preservation u Ξ±)
\end{code}

Some shorthands to simplify examples of system T terms.

\begin{code}

numeral : {n : β„•} {Ξ“ : Cxt n} β†’ β„• β†’ T Ξ“ ΞΉ
numeral 0        = Zero
numeral (succ n) = Succ Β· (numeral n)

Ξ½β‚€ : {n : β„•} {Ξ“ : Cxt(succ n)} β†’ T Ξ“ (Ξ“ [ 𝟎 ])
Ξ½β‚€ = Ξ½ 𝟎

ν₁ : {n : β„•} {Ξ“ : Cxt(succ (succ n))} β†’ T Ξ“ (Ξ“ [ suc 𝟎 ])
ν₁ = Ξ½ (suc 𝟎)

Ξ½β‚‚ : {n : β„•} {Ξ“ : Cxt(succ (succ (succ n)))}
   β†’ T Ξ“ (Ξ“ [ suc (suc 𝟎) ])
Ξ½β‚‚ = Ξ½ (suc (suc 𝟎))

ν₃ : {n : β„•} {Ξ“ : Cxt(succ (succ (succ (succ n))))}
   β†’ T Ξ“ (Ξ“ [ suc (suc (suc 𝟎)) ])
ν₃ = Ξ½ (suc (suc (suc 𝟎)))

Ξ½β‚„ : {n : β„•} {Ξ“ : Cxt(succ (succ (succ (succ (succ n)))))}
   β†’ T Ξ“ (Ξ“ [ suc (suc (suc (suc 𝟎))) ])
Ξ½β‚„ = Ξ½ (suc (suc (suc (suc 𝟎))))

\end{code}