Contents Previous Next


Gödel’s T

open import Types.equality renaming (¬ to ¬-eq)
open import Level using (0ℓ)
open import Types.product using (__)

module AppliedTypes.godels_t where

“Gödel’s T”, also known as “System T”, named after the mathematician Kurt Gödel, is a formal system designed by Gödel to provide a consistency proof of arithmetic. This system includes a type system based on booleans and natural numbers and allows primitive recursion.

System T basically consists of natural numbers:

data: Set where
  zero :
  succ :

booleans:

data Bool : Set where
  true  : Bool
  false : Bool

if-then-else:

if_then_else_ : {C : Set}  Bool  C  C  C
if true  then x else y = x
if false then x else y = y

and recursion on natural numbers:

recₙ : {x : Set}  x  ( x  x)  x
recₙ p h  zero    = p
recₙ p h (succ n) = h n (recₙ p h n)

Binary operations

Addition and multiplication on natural numbers can be defined via recursion:

_+_ :
_+_ n m = recₙ m  x y  succ y) n

_*_ :
_*_ n m = recₙ zero  x y  y + m) n

-- opposite direction of succ
prev :
prev n = recₙ n  x y  x) n

__ :
__ n m = recₙ n  x y  (prev y)) m

data __ : Rel ℕ 0ℓ where
  z≤n :  {n}                  zero  ≤ n
  s≤s :  {m n} (m≤n : m ≤ n)  succ m ≤ succ n

_<_ : Rel ℕ 0ℓ
m < n = succ m ≤ n

_>_ : Rel ℕ 0ℓ
m > n = n < m

Boolean operators can be built on top of if-then-else:

¬ : Bool  Bool
¬ b = if b then false else true

__ : Bool  Bool  Bool
a ∧ b = if a then b else false

__ : Bool  Bool  Bool
a ∨ b = if a then true else b

__ : Bool  Bool  Bool
a ⊕ b = if a then (¬ b) else b

Prime numbers

A prime number is defined as a natural number with only two divisors - 1 and itself.

-- divisibility
infix 4 __ __

record __ (m n :) : Set where
  constructor divides
  field
    quotient :
    equality : n ≡ quotient * m
open __ using (quotient) public

__ : Rel ℕ 0ℓ
m ∤ n = ¬-eq (m ∣ n)

Prime number definition:

record Prime (p :) : Set where
  constructor prime
  field
    -- primes > 2
    p>1 : p > (succ zero)
    -- only 2 divisors - 1 and p
    isPrime  :  {d}  d ∣ p  (d ≡ (succ zero))(d ≡ p)

Definability

A function $ f : ℕ → ℕ $ is definable if one can find an expression e of f such that:

∀ x ∈ ℕ, f(x) ≡ e(x)

or in other words, if one can implement the function in system T using only if-then-else and primitive recursion.

If we were to assign a natural number to each such implementation of every function possible, we can treat each expression as data:

count = zero
one = succ zero

assign : (ℕ → ℕ) → ℕ
assign f = count + one

System F