Editing Lambda cube (section)

== Relation to other systems ==
The system [[Automath]] is similar to λ2 from a logical point of view. The [[ML (programming language)|ML-like languages]], from a typing point of view, lie somewhere between λ→ and λ2, as they admit a restricted kind of polymorphic types, that is the types in prenex normal form. However, because they feature some recursion operators, their computing power is greater than that of λ2.<ref name=":1" /> The Coq system is based on an extension of λC with a linear hierarchy of universes, rather than only one untypable <math display="inline">\square</math>, and the ability to construct inductive types.

[[Pure type system]]s can be seen as a generalization of the cube, with an arbitrary set of sorts, axiom, product and abstraction rules. Conversely, the systems of the lambda cube can be expressed as pure type systems with two sorts <math>\{*, \square\}</math>, the only axiom <math display="inline">\{*,\square\}</math>, and a set of rules <math display="inline">R</math> such that <math>\{(*,*,*)\} \subseteq R \subseteq \{(*,*,*), (*,\square, \square), (\square, *, *), (\square, \square, \square) \}</math>.<ref name=":0" />

Via the Curry-Howard isomorphism, there is a one-to-one correspondence between the systems in the lambda cube and logical systems,<ref name=":0" /> namely:
{| class="wikitable"
!System of the cube
!Logical System
|-
|λ→
|(Zeroth-order) [[Propositional calculus|Propositional Calculus]]
|-
|λ2
|[[Second-order propositional logic|Second-order Propositional Calculus]]
|-
|λ{{Underline|ω}}
|Weakly Higher Order Propositional Calculus
|-
|λω
|Higher Order Propositional Calculus
|-
|λP
|(First order) [[Predicate Logic]]
|-
|λP2
|[[Second order predicate calculus|Second-order Predicate Calculus]]
|-
|λP{{Underline|ω}}
|Weak [[Higher-order logic|Higher Order Predicate Calculus]]
|-
|λC
|[[Calculus of constructions|Calculus of Constructions]]
|}
All the logics are implicative (i.e. the only connectives are <math display="inline">\to</math> and <math display="inline">\forall</math>), however one can define other connectives such as <math>\wedge</math> or <math>\neg</math> in an [[impredicative]] way in second and higher order logics. In the weak higher order logics, there are variables for higher order predicates, but no quantification on those can be done.