Intuitionistic Type Theory - Formalisation of Type Theory

Formalisation of Type Theory

This formalization is based on the discussion in Nordstrom, Petersson, and Smith.

The formal theory works with types and objects.

A type is declared by:

An object exists and is in a type if:

Objects can be equal

and types can be equal

A type that depends on an object from another type is declared

and removed by substitution

• , replacing the variable with the object in .

An object that depends on an object from another type can be done two ways. If the object is "abstracted", then it is written

and removed by substitution

• , replacing the variable with the object in .

The object-depending-on-object can also be declared as a constant as part of a recursive type. An example of a recursive type is:

Here, is a constant object-depending-on-object. It is not associated with an abstraction. Constants like can be removed by defining equality. Here the relationship with addition is defined using equality and using pattern matching to handle the recursive aspect of .

is manipulated as a opaque constant - it has no internal structure for substitution.

So, objects and types and these relations are used to express formulae in the theory. The following styles of judgements are used to create new objects, types and relations from existing ones.

• , is a well-formed type in context .
• , is a well-formed term of type in context .
• , and are equal types in context .
• , and are equal terms of type in context .
• , is a well-formed context of typing assumptions.

By convention, there is a type that represents all other types. It is called (or ). Since is a type, the member of it are objects. There is a dependent type that maps each object to its corresponding type. In most texts is never written. From the context of the statement, a reader can almost always tell whether refers to a type, or whether it refers to the object in that corresponds to the type.

This is the complete foundation of the theory. Everything else is derived.

To implement logic, each proposition is given its own type. The objects in those types represent the different possible ways to prove the proposition. Obviously, if there is no proof for the proposition, then the type has no objects in it. Operators like "and" and "or" that work on propositions introduce new types and new objects. So is a type that depends on the type and the type . The objects in that dependent type are defined to exist for every pair of objects in and . Obviously, if or has no proof and is an empty type, then the new type representing is also empty.

This can be done for other types (booleans, natural numbers, etc.) and their operators.