# 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