HOL

HOL known as Higher Order Lambda, is a language that combines higher order logic with typed lambda calculus. The goal is to be extremely powerful model of mathematics and computation while being extremely well-defined.

Objects and Syntax

There are two types of objects: terms and types. Let's start with the types first: in BNF the types are:

T ::= (T → T) | nat

Next are the terms. We have the basic typing rules where a:A means "a has type A":

x:X and y:Y, then λx.y has type (X → Y)
x:(X → Y) and y:X, then xy has type Y
x:nat and y:nat, then xy has type nat
x:nat and y:(Y → Y), then xy has type (Y → Y)

Next are the basic constants:

0 : nat
S : nat → nat
M1 : (nat → nat) → nat
M2 : ((nat → nat) → nat) → nat
M3 : (((nat → nat) → nat) → nat) → nat
Mm+1 : typeOf[Mm] → nat

In words: we use the regular STLC but we add a new construct called nat which functionally acts like ∀x.((x→x)→x→x) where it takes in any function with same domain/codomain and outputs an iterated version of it. We then add the zero constant the the successor function S. We also add an infinite class of M_i where each successive element is more complex than the previous.

Semantics

The semantics are as followed:

Regular typed lambda calculus rules are followed
0 F x = x
S n F x = f (n f x)

However, to define M_i we must define the following collections:

N1 = ℕ
N2 = Collection of all functions from N1 to ℕ
N3 = Collection of all functions from N2 to ℕ
N4 = Collection of all functions from N3 to ℕ
Nm+1 = Collection of all functions from Nm to ℕ

Then we define:

Mi F = max{F α | α ∈ Ni} if exists, otherwise Mi F = 0

Complexity Class

Simply Typed lambda calculus is not Turing complete on its own but by adding natural numbers we are able to reach the strength of Peano arithmetic and thus can express any primitive recursive function.

M₁ originally seems to work like the classic minimization operator (we can for instance have a function that is the identity function until a trigger point and then zero afterwards, and that effectively acts like minimization). More broadly though, M_i works like the i-th order existential quantifier because we can let 0 be false and 1 be true, and taking the maximum over a set of expressions is essentially testing whether one of the expressions return a nonzero value.

This is actually enough to fully reach higher order logic. As a bonus, STLC is strongly normalizing and adding nat is also strongly normalizing because System F is consistent. Adding M_i still preserves totality but M_i is uncomputable due to extreme quantification. One can observe:

• M₁ can quantify over the natural numbers
• M₂ can quantify over the real numbers
• M₃ can quantify over the functions of real numbers
• M₄ can quantify over the power set of the functions of real numbers

For example, it is possible to write a program that returns 1 if the continuum hypothesis is true and 0 otherwise. Nonetheless, we believe to be a "standard" model of higher order arithmetic, where every expression has a value.