Yes, I quite realize, being something of a type-theory geek myself. What System F is not is a dependent type theory, with a proposition type and strong normalization, or even a propositional fragment in which proofs must normalize, or types dependent on values (which you need, in order to get proper propositional reasoning!).
A self-interpreting variant on Martin-Loef or Homotopy Type Theory would have been astounding! But that’s not what this is.
Decidability is not actually what we want here :-p. I could go into elaborate descriptions of what we want, but those would be theory-laden with my own ideas. Read my backlog on here to get an idea of the general direction I’m thinking in.
This result is not trivial, but it’s useful for talking about Turing-complete programming languages, not about logic.
Yes, I quite realize, being something of a type-theory geek myself. What System F is not is a dependent type theory, with a proposition type and strong normalization, or even a propositional fragment in which proofs must normalize, or types dependent on values (which you need, in order to get proper propositional reasoning!).
A self-interpreting variant on Martin-Loef or Homotopy Type Theory would have been astounding! But that’s not what this is.
Decidability has a price. So apparently you are dissatisfied by this result or consider it trivial. I think this buys a lot. Waht are you missing?
Decidability is not actually what we want here :-p. I could go into elaborate descriptions of what we want, but those would be theory-laden with my own ideas. Read my backlog on here to get an idea of the general direction I’m thinking in.
This result is not trivial, but it’s useful for talking about Turing-complete programming languages, not about logic.