I have been trying to learn about the lambda cube, but cannot find any sources covering the P weak omega and P2 nodes. Is the problem that these nodes are not frequently used/ offer little benefits over the calculus of constructions? Thanks

  • 1
    $\begingroup$ What's the "P weak omega"? Can you link to the reference you have in mind? $\endgroup$
    – cody
    Commented Jan 31 at 14:28
  • $\begingroup$ It is mentioned in "An Introduction to generalized type systems" in the journal of Functional Programming, April 1991. homepages.inf.ed.ac.uk/wadler/papers/barendregt/… mentioned on page five of the linked PDF. Thank you :) $\endgroup$
    – hugofin
    Commented Feb 2 at 20:10

1 Answer 1


I've talked about a couple of these in this question, though Neel's answer gives a lot of insight as well, though I didn't dwell on $\lambda P_\underline{\omega}$ specifically.

$\lambda P_2$ is quite famous: it's the dependent type theory corresponding to second-order predicate logic. I think Geuvers has written about it (e.g. here. It's a good place to do math in, in fact you pretty rarely need the extra power of the CoC, though it is convenient.

$\lambda P_\underline\omega$ is not second order, so you cannot quantify over predicates, e.g. as in $\forall P:\star, P \rightarrow P$, indeed you only have a little more expressive power over simple first order logic.

One thing you can do in this system is express predicate transformers. For example, in the context $\mathbb{N} : \star$ one could declare

$$\mathrm{Exists}:(\mathbb{N}\rightarrow \star)\rightarrow \star$$

That is, you can give a type to the $\exists$ operator, which is not possible in $\lambda P$ proper.

I'm not sure anyone's studied this system on its own though.

Edit (7/8/2024)

One thing that might be worth noting, is that while $\lambda P_{\underline\omega}$ is slightly more expressive than the "simple" dependent type theory $\lambda P$ (below it in the Barendregt cube), it is not more powerful in the sense that:

Everything provable in $\lambda P_{\underline\omega}$ that can be expressed in $\lambda P$ can already be proven in $\lambda P$.

That is to say, $\lambda P_{\underline\omega}$ is conservative over $\lambda P$. This can be proven via a relatively straightforward normalization argument (of the type-level expressions).

  • $\begingroup$ Wow, thank you! that thread and the article is very useful. I couldnt quite believe that nobody had published any papers on lambda P weak omega ever so wanted to make sure. $\endgroup$
    – hugofin
    Commented Feb 4 at 19:12
  • $\begingroup$ I don't know of any work that looks at it specifically. $\endgroup$
    – cody
    Commented Feb 5 at 16:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.