1
$\begingroup$

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?

Improve this question
$\endgroup$
2
  • $\begingroup$ Your characterization is going to necessarily have to be a bit soft, or presuppose a little about what "stating quantification" means: e.g. since inhabitation in System F is undecidable, you could always code arithmetic $\Pi^0_1$ sentences in a very awkward way. $\endgroup$
    – cody
    Commented Sep 8 at 2:44
  • 1
    $\begingroup$ Cross-posted here cstheory.stackexchange.com/questions/54642/… and here: math.stackexchange.com/questions/4968748/… Please don't do this. And Andrej said on CSTheory.SE, please pick one to keep. I recommend that one, since I think you'll get more luck there. $\endgroup$
    – David Roberts ♦
    Commented Sep 9 at 10:13

0

Reset to default

Browse other questions tagged .