All Questions

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 ...

Summary My question is about how (i) a certain presentation of pure type systems in the $\lambda$-cube, bears on (ii) a standard definition of consistency in pure type systems. In short, I'm ...

Pure type systems are characterized in an almost combinatorial way: a set of axioms $\star_i : \star_j$, and a set of triples $(\star_i, \star_j, \star_k)$ saying when the dependent product $\prod_{x :...

Godel's system $T$ means different, although equivalent, things to different people. To people working in the traditon of mathematical logic, $T$ is a quantifier-free equational theory of arithmetic ...

It is well-known that the simply typed lambda calculus is strongly normalizing (for instance, Wikipedia). Hence, it is not strong enough to be Turing-complete, as also mentioned on the Wikipedia page ...

I've been reading Girard et al's 'Proofs and Types', which in Chapter 6 presents a proof of strong normalisation for the simply typed lambda calculus with products and base types. The proof is based ...