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