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

Question

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

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.