A simple question here, which likely demands a somewhat complex answer... Or rather, a set of related questions.
- What are the advantages of typed lambda calculus over untyped lambda calculus in terms of proof theory?
- Specifically, Church's original Lambda Calculus was untyped and allows arbitrarily high-order functions. What are the limitations with respect to constructing a proof calculus from it?
- Are not untyped and typed lambda calculi inherently higher-order formal systems?
- What are the reasons for using complex (e.g. polymorphic/dependent) type theories over the simple type theory in lambda calculus? Are they more 'powerful' in some sense; if so, how exactly?
- Do semantics (interpretation) have anything to say here, with respect to typed and untyped theories, especially in terms of soundness and completeness?
- The well-known proof verifier Coq, which (I believe) uses a language of higher-order complex-typed lambda calculus to represent proofs in constructive (intuistionistic) mathematics. I have read that the theory behind it (the Calculus of Constructions) is essentially an extension of the Curry-Howard isomorphism to higher-order logic. Are there any elaborations/clarifications I should be aware of here?