In my searching, I've seen that if Church numerals are encoded in a dependently typed Lambda calculus, that we can't derive induction or that $0 \neq 1$.

I know that LF and the dependently typed Lambda calculus (from the Lambda cube) are often used to model logic, but any actual systems I've seen based on this augment it with inductive data types, propositional equality, etc.

I'm wondering, can anything non-trivial be done in a pure dependently typed Lambda calculus, without adding inductive types or such? I.e. is there anything we can encode (i.e. length indexed vectors, equality, etc) and prove things about in a dependently typed lambda system that we can't in a Simply Typed System, or something like System F?

I know that dependent types don't give us anything extra for computability, but I'm wondering about expressiveness.

  • $\begingroup$ I don't say this often, but shouldn't this question be on cstheory.stackexchange.com? $\endgroup$ – Andrej Bauer Oct 13 '18 at 21:35
  • $\begingroup$ I'd first try to give a precise technical meaning to "interesting terms". One way of doing that would be to give a precise meaning to the question "Are there any interesting terms in the simply typed $\lambda$-calculus?" and then generalize it to $\lambda\Pi$. $\endgroup$ – Andrej Bauer Oct 13 '18 at 21:39
  • $\begingroup$ When you say "pure", what sort of base types and base families do you allow? $\endgroup$ – Andrej Bauer Oct 13 '18 at 21:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.