<p>I've talked about a couple of these in <a href="https://cstheory.stackexchange.com/q/36054/3984">this</a> question, though Neel's answer gives a lot of insight as well, though I didn't dwell on <span class="math-container">$\lambda P_\underline{\omega}$</span> specifically.</p>
<p><span class="math-container">$\lambda P_2$</span> is quite famous: it's the dependent type theory corresponding to second-order predicate logic. I think Geuvers has written about it (e.g. <a href="http://www.cs.ru.nl/%7Eherman/PUBS/IndNonder.pdf" rel="nofollow noreferrer">here</a>. 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.</p>
<p><span class="math-container">$\lambda P_\underline\omega$</span> is <em>not</em> second order, so you cannot quantify over predicates, e.g. as in <span class="math-container">$\forall P:\star, P \rightarrow P$</span>, indeed you only have a little more expressive power over simple first order logic.</p>
<p>One thing you <em>can</em> do in this system is express <em>predicate transformers</em>. For example, in the context <span class="math-container">$\mathbb{N} : \star$</span> one could declare</p>
<p><span class="math-container">$$\mathrm{Exists}:(\mathbb{N}\rightarrow \star)\rightarrow \star$$</span></p>
<p>That is, you can give a type to the <span class="math-container">$\exists$</span> operator, which is not possible in <span class="math-container">$\lambda P$</span> proper.</p>
<p>I'm not sure anyone's studied this system on its own though.</p>
<hr />
<p><strong>Edit</strong> (7/8/2024)</p>
<p>One thing that might be worth noting, is that while <span class="math-container">$\lambda P_{\underline\omega}$</span> is slightly more <em>expressive</em> than the &quot;simple&quot; dependent type theory <span class="math-container">$\lambda P$</span> (below it in the Barendregt cube), it is not more <em>powerful</em> in the sense that:</p>
<blockquote>
<p>Everything provable in <span class="math-container">$\lambda P_{\underline\omega}$</span> that can be expressed in <span class="math-container">$\lambda P$</span> can already be proven in <span class="math-container">$\lambda P$</span>.</p>
</blockquote>
<p>That is to say, <span class="math-container">$\lambda P_{\underline\omega}$</span> is <em>conservative</em> over <span class="math-container">$\lambda P$</span>. This can be proven via a relatively straightforward normalization argument (of the <em>type-level</em> expressions).</p>

CC BY-SA 4.0
2024-02-04T19:12:45.327Z
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.
hugofin
CC BY-SA 4.0
2024-02-05T16:20:00.300Z
I don't know of any work that looks at it specifically.
cody
CC BY-SA 4.0
2024-02-04T03:17:03.680Z
2024-07-08T17:13:44.387Z
2024-07-08T17:13:44.387Z
cody
<p>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</p>

CC BY-SA 4.0
2024-01-31T14:28:50.573Z
What's the "P weak omega"? Can you link to the reference you have in mind?
cody
CC BY-SA 4.0
2024-02-02T20:10:01.050Z
It is mentioned in "An Introduction to generalized type systems" in the journal of Functional Programming, April 1991.  https://homepages.inf.ed.ac.uk/wadler/papers/barendregt/pure-type-systems.pdf mentioned on page five of the linked PDF.  Thank you :)
hugofin
<lambda-calculus><dependent-type><typed-lambda-calculus>
Are there any books or articles that contain information on the P weak omega or second order predicate calculi?
hugofin
# Are there any books or articles that contain information on the P weak omega or second order predicate calculi?

(Asked by: username_0 on 2024-01-31)

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

**Tags:** lambda-calculus, dependent-type, typed-lambda-calculus

> **Comments:**
> **username_1**: What's the "P weak omega"? Can you link to the reference you have in mind?  
> **username_0**: It is mentioned in "An Introduction to generalized type systems" in the journal of Functional Programming, April 1991.  https://homepages.inf.ed.ac.uk/wadler/papers/barendregt/pure-type-systems.pdf mentioned on page five of the linked PDF.  Thank you :)  

---

## 1 answers

### Answer by username_1 on 2024-02-04. Score: 5

I've talked about a couple of these in [this](https://cstheory.stackexchange.com/q/36054/3984) 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](http://www.cs.ru.nl/%7Eherman/PUBS/IndNonder.pdf). 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).

> **Comments:**
> **username_0**: 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.  
> **username_1**: I don't know of any work that looks at it specifically.  

---

