<p>I'm trying to understand exactly why it is that <a href="https://ncatlab.org/nlab/show/computational+trilogy" rel="nofollow noreferrer">https://ncatlab.org/nlab/show/computational+trilogy</a> states that quantification requires dependent types, and why this wouldn't be possible to achieve with System F. From what I've managed to gather, System F can express quantification, but only over types, and not over elements or predicates.</p>
<p>I'm looking for a way to formalize this statement in order to start working on a proof. How could I express: System F lacks the expressive power to state quantification over terms? Or, lacks the expressive power to state quantification in the way made possible by dependent types?</p>

CC BY-SA 4.0
2024-09-08T14:36:19.847Z
cross-posted from mathover and math stackexchange
shintuku
CC BY-SA 4.0
2024-09-08T14:42:29.880Z
Do not cross-post, it's impolite. Pick one site and delete the other two. Also, in order to speak of quantification over terms, you first need to explain what a predicate/type on terms is supposed to be in System F, so that we can then quantify over them.
Andrej Bauer
CC BY-SA 4.0
2024-09-08T14:44:24.623Z
@AndrejBauer sorry!
shintuku
CC BY-SA 4.0
2024-09-09T10:13:40.457Z
https://math.stackexchange.com/questions/4968748/how-could-i-formally-express-system-f-cannot-express-universal-quantification-o and https://mathoverflow.net/questions/478414/how-could-i-formally-express-system-f-cannot-express-universal-quantification-o
David Roberts
<lo.logic><lambda-calculus><typed-lambda-calculus>
How could I formally express: System F cannot express universal quantification over things that are not types?
shintuku
# How could I formally express: System F cannot express universal quantification over things that are not types?

(Asked by: username_0 on 2024-09-08)

I'm trying to understand exactly why it is that <https://ncatlab.org/nlab/show/computational+trilogy> states that quantification requires dependent types, and why this wouldn't be possible to achieve with System F. From what I've managed to gather, System F can express quantification, but only over types, and not over elements or predicates.

I'm looking for a way to formalize this statement in order to start working on a proof. How could I express: System F lacks the expressive power to state quantification over terms? Or, lacks the expressive power to state quantification in the way made possible by dependent types?

**Tags:** lo.logic, lambda-calculus, typed-lambda-calculus
> **Comments:**
> **username_0**: cross-posted from mathover and math stackexchange  
> **username_1**: Do not cross-post, it's impolite. Pick one site and delete the other two. Also, in order to speak of quantification over terms, you first need to explain what a predicate/type on terms is supposed to be in System F, so that we can then quantify over them.  
> **username_0**: @AndrejBauer sorry!  
> **username_2**: https://math.stackexchange.com/questions/4968748/how-could-i-formally-express-system-f-cannot-express-universal-quantification-o and https://mathoverflow.net/questions/478414/how-could-i-formally-express-system-f-cannot-express-universal-quantification-o  

---

## 0 answers

