# Are there any books or articles that contain information on the P weak omega or second order predicate calculi?

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

• What's the "P weak omega"? Can you link to the reference you have in mind?
– cody
Jan 31 at 14:28
• 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 :) Feb 2 at 20:10

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.

• 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. Feb 4 at 19:12
• I don't know of any work that looks at it specifically.
– cody
Feb 5 at 16:20