System U

In mathematical logic, System U and System U− are pure type systems, i.e. special forms of a typed lambda calculus with an arbitrary number of sorts, axioms and rules (or dependencies between the sorts).

System U was proved inconsistent by Jean-Yves Girard in 1972 (and the question of consistency of System U− was formulated). This result led to the realization that Martin-Löf's original 1971 type theory was inconsistent, as it allowed the same "type in type" behaviour that Girard's paradox exploits.

Formal definition

System U is defined as a pure type system with

three sorts

{

∗

,

◻

,

△

}

{\displaystyle \{\ast ,\square ,\triangle \}}

;

two axioms

{

∗

:

◻

,

◻

:

△

}

{\displaystyle \{\ast :\square ,\square :\triangle \}}

; and

five rules

{

(

∗

,

∗

)

,

(

◻

,

∗

)

,

(

◻

,

◻

)

,

(

△

,

∗

)

,

(

△

,

◻

)

}

{\displaystyle \{(\ast ,\ast ),(\square ,\ast ),(\square ,\square ),(\triangle ,\ast ),(\triangle ,\square )\}}

.

System U− is defined the same with the exception of the

(

△

,

∗

)

{\displaystyle (\triangle ,\ast )}

rule.

The sorts

∗

{\displaystyle \ast }

and

◻

{\displaystyle \square }

are conventionally called “type” and “kind”, respectively; the sort

△

{\displaystyle \triangle }

doesn't have a specific name. The two axioms describe the containment of types in kinds (

∗

:

◻

{\displaystyle \ast :\square }

) and kinds in

△

{\displaystyle \triangle }

(

◻

:

△

{\displaystyle \square :\triangle }

). Intuitively, the sorts describe a hierarchy in the nature of the terms.

All values have a type, such as a base type (e.g.