The Power of Lambda Calculi

Solution 1:

1. What are the advantages of typed lambda calculus over untyped lambda calculus in terms of proof theory? and also
2. 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?
   • Simply, typed lambda calculus has a proof theory, and untyped lambda calculus doesn't because it lacks a normal-form theorem.
3. Are not untyped and typed lambda calculi inherently higher-order formal systems?
   • This is tricky, because there are two ways of looking at higher-orderness. They are higher-order when you look at the terms, since the definition of higher order is abstraction over higher-order entities like functions, and lambda abstraction is abstraction. But note, under the formulae-as-types correspondence, the proposaitions in logic are associated with the types of the lambda terms, and in, say, the simply-typed lambda calculus, there is no abstraction over anything. This point confused me when I first studied Church's simple theory of types, because it is a higher-order calculus based on simply-typed lambda calculus, where the propositions are formed using the lambda terms, rather than, as with the formulae-as-types corespondence, being the types.
4. 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?
   • They do add power. Under the formulae-as-types correspondence, the simply-typed lambda calculus has as its matching logic propositional calculus, adding dependent types adds universal and existential quantification at higher finite types to its logic. Polymorphic types allow types allowing all usual mathematical entities to be constructed (although without the usual theory of provability) and has high proof-theoretic consistency: Strong normalisation of system F has (over a base theory such as RCL0) the same strength as consistency second order arithmetic, even though it lacks an induction principle.
5. Do semantics (interpretation) have anything to say here, with respect to typed and untyped theories, especially in terms of soundness and completeness?
   • They are much less useful with these sorts of theories than model theory is with classical logic, although there are good applications of category theory to the semantics of type theory.
6. 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?
   • Yes, that polymorphic types are tricky, and non-conservative over the base theory. I'd recommend sarting an exploration of formulae-as-types with Martin-Löf's dependent type theory. If you want to work with a proof assistant, there is Agda, which is a functional programming language whose type system is Martin-Löf's type theory.