```
open import Types.relations renaming (¬_ to ¬-eq_)
open import Types.equality
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
: Bool
true : Bool false
```

if-then-else:

```
_then_else_ : {C : Set} → Bool → C → C → C
if= x
if true then x else y = y if false then x else y
```

and recursion on natural numbers:

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

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 = recₙ n (λ x y → x) n
prev n
_−_ : ℕ → ℕ → ℕ
_−_ n m = recₙ n (λ x y → (prev y)) m
data _≤_ : Rel ℕ 0ℓ where
: ∀ {n} → zero ≤ n
z≤n : ∀ {m n} (m≤n : m ≤ n) → succ m ≤ succ n
s≤s
_<_ : Rel ℕ 0ℓ
= succ m ≤ n
m < n
_>_ : Rel ℕ 0ℓ
= n < m m > n
```

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

```
: Bool → Bool
¬ = if b then false else true
¬ b
_∧_ : Bool → Bool → Bool
= if a then b else false
a ∧ b
_∨_ : Bool → Bool → Bool
= if a then true else b
a ∨ b
_⊕_ : Bool → Bool → Bool
= if a then (¬ b) else b a ⊕ b
```

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 : n ≡ quotient * m
equality open _∣_ using (quotient) public
_∤_ : Rel ℕ 0ℓ
= ¬-eq (m ∣ n) m ∤ n
```

Prime number definition:

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

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
```