Skip to main content
10 votes

Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic

I do not know if this answers your question, but in Propositions as [Types] we communicate in Remark 6.6 an observation by Thierry Coquand, namely that the statement $$ (\forall x .\, \exists y .\, R(...
Andrej Bauer's user avatar
  • 28.9k
2 votes
Accepted

Isn't it misleading for Scala 3 to claim it has dependent function types?

In my interpretation of how Scala types can be translated to type theory, a trait is a type and an instance of the trait is a subtype. Therefore, in the example above, ...
nickie's user avatar
  • 256
1 vote

How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)?

The question is about dependent type theory, but, if the type you are trying to show non-inhabited can be expressed as a first-order formula, you can also use classical logic. You either prove ...
Danko Ilik's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible