- What exactly is the role of type theory in creating higher-order logics? Same goes with category theory/model theory, which I believe is an alternative.
Don't think of type theory, categorical logic, and model theory as alternatives to one another. Each step on the progression forgets progressively more structure, and whether that structure is essence or clutter depends on the problem you are trying to solve. Roughly speaking, the two poles are type theory and model theory, which focus on proofs and provability, respectively.
To a model theorist, two propositions are the same if they have the same provability/truth value. To a type theorist, equisatisfiability means that we have a proof of the biimplication, which is obviously not the same thing as the propositions being the same. (In fact, even the right notion of equivalence for proofs is still not settled to type theorists' satisfaction.)
Categorical logicians tend to move between these two poles; on the one hand, gadgets like Lawvere doctrines and topoi are essentially model-theoretic, since they are provability models. On the other hand, gadgets like cartesian closed categories give models of proofs, up to $\beta\eta$-equivalence.
- Is extending a) natural deduction, b) sequent calculus, or c) some other formal system the best way to go for creating higher order logics?
It depends on what you are doing. If you are building a computerized tool, then typically either natural deduction or sequent calculus is the way to go, because these calculi both line up with human practice and help constrain proof search in ways helpful to computers. It makes sense to cook up a sequent calculus or natural deduction system even if the theory you want to use (e.g., set theory) is not normally cast in these terms.
On the other hand, model theory has been spectacularly successful in applications to mathematics, and this is in part because it does not have a built-in notion of proof system -- so there is simply less machinery you need to reinterpret before you can apply it to a mathematical problem. (The corresponding use of type theory is much less developed; homotopy theorists are in the very earliest stages of turning dependent type theory into ordinary mathematics.)
- Where does typed lambda calculus come into proof verification?
Every well-behaved intuitionistic logic has a corresponding typed lambda calculus. See Sorensen and Urcyczyn's Lectures on the Curry-Howard Correspondence for (many) more details.
- Are there any other approaches than higher order logic to proof verification?
Yes and no. If you're interested in actual, serious mathematics, then there is no alternative to HOL or the moral equivalent (such as dependent type theory or set theory) because mathematics deals intrinsically with higher-order concepts.
However, large portions of any development involve no logically or conceptually complex arguments: they are just symbol management, often involving decidable theories. This is often amenable to automation, if the problems in question are not stated in unnaturally higher-order language. (Sometimes, as in the case of the Kepler conjecture, there is an artificial way of stating the problem in a simple theory. This is essentially the reason why Hales' proof relies so heavily on computers: he very carefully reduced the Kepler conjecture to a collection of machine-checkable statements about real closed fields.)
- What are the limitations/shortcomings of existing proof verification systems (see below)?
The main difficulty with these tools is finding the right balance between automation and abstraction. Basically, the more expressive the logic, the harder automated proof search becomes, and the more easily and naturally you can define abstract theories that can be used in many different contexts.
The simply-typed $\lambda$-calculus is not stronger than second-order logic.
The simply-typed $\lambda$-calculus has:
- product types $A \times B$, with corresponding term formers (pairing and projections)
- function types $A \to B$, with corresponding term formers (abstraction and application)
- equations governing the term formers and subtitution
The simply-typed $\lambda$-calculus does not postulate the existence of any types. Sometimes we postulate the unit type $1$, and often we postulate the existence of a collection of basic types, but without any assumptions about them being inhabited. This is akin to using a collection of propositional symbols in the propositional calculus, where we make no claims as to their truth value.
Simple type theory is simply-typed $\lambda$-calculus and additionally at least:
- the type of truth values $o$, with the corresponding term formers (constants $\bot$ and $\top$, connectives, quantifiers at every type)
- the type of natural numbers $\iota$, with the corresponding term formers (zero, succcesor, primitive recursion into arbitrary types)
- equations governing the term formers and substitution
There are several variations:
- we may postulate excluded middle for truth values
- we may include a definite description operator
- we may include the axiom of choice
- we may vary the extensionality principles
We quickly obtain a formal system that expresses Heyting (or Peano) arithmetic and more, which suffices for incompleteness phenomena to kick in.
What I think is confusing you is the fact that there are two ways to relate logic to type theory:
The Curry-Howard correspondence relates the propositional calculus to the simply-typed $\lambda$-calculus by an interpreation of propositional formulas as types.
Higher-order logic embeds into simple type theory by an interpretation of logical formulas as terms of the type $o$ of truth values.
There is a difference of levels, which makes all the difference.
To illustrate, consider the propositional formula
$$p \land q \Rightarrow (r \Rightarrow p \land r).$$
In the simply typed $\lambda$-calculus it is interpreted as the type
$$P \times Q \to (R \to P \times R).$$
To prove the formula amounts to giving a term of the type.
In constrast, in simple type theory it is interpreted as the term
$$p \land q \Rightarrow (r \Rightarrow p \land r) : o$$
(with parameters $p, q, r$ of type $o$).
Now proving the formula amounts to proving the equation $(p \land q \Rightarrow (r \Rightarrow p \land r)) =_o \top$ in the simple type theory.
A higher-order formula, such as $(\forall r : \mathsf{Prop} . r \Rightarrow p) \Rightarrow p$ cannot be encoded in the simply-typed $\lambda$-calculus, whereas in the simple type theory it is again just a term of type $o$ (just replace the sort of propositions $\mathsf{Prop}$ with the type $o$).
Also note that the pure simply-typed $\lambda$-calculus does not postulate the natural numbers. If we add the natural numbers to the simply-typed $\lambda$-calculus we get a fragment of simple type theory known as Gödel's System T (or a version of it, depending on minutiae of how equality is treated), which suffers from – or enjoys, depending on your point of view – the incompleteness phenomena already.
Best Answer
Here are some further possibilites:
Propositional logic: can be interpreted in any Boolean algebra (assuming you are talking about classical logic here), but perhaps your notion of truth assignment allows for truth values as elements of Boolean algebras. Alternatively, via the Curry-Howard correspondence propositions may be interpreted as types and proofs as terms of those types.
Predicate logic (first-order and higher-order): can in general be interpreted in suitable categories or fibrations. For example, higher-order logic can be interpreted in a topos (which must be Boolean if your logic is classical).
In general, if you are looking for interpretations of various kinds of logic in ways other than first-order model theory, you should look at categorical logic. There various possibilities (multi-sorted vs. single-sorted, intuitionistic vs. classical, etc) are systematically considered. Also, the ad-hoc distinction between "full" vs. "Henkin-style" semantics (which depends on the idea that there is a "true" set theory in the background, as far as I can tell) is replaced with a much more advanced notions (such as properties of fibrations that are used to interpret logic). A place to start looking would be Bart Jacob's "Categorical logic and type theory", although it's not an easy reading. There should be some lecture notes on the internet that are more accessible, perhaps someone can suggest them?
I am not sure what you mean by "valid interpretation". If you just mean soundness (provable things are valid) then all of the possibilities mentiond are "valid". But I suspect you mean something else.