Categorical equivalent of higher order logic

Question

From Simply typed lambda calculus and higher order logic, I get the impression that HOL is STLC + equality + equality axioms. I was wondering if there is a particular kind of category modelling this.

Answer 1

It seems to me there isn't an agreement about what "HOL" means. The OP indicates in their question that they are thinking of the formalization of higher-order logic within the formalism of the simply-typed $\lambda$-calculus. To give the question some clarity, allow me to spell out my understanding of what such a formalism comprises.

Recall the notion of a theory in first-order logic. It is given by function symbols, relation symbols, and axioms. This pattern is repeated in many other formalisms, including the simply typed $\lambda$-calculus.

A theory of STLC is given by a collection of type consants and term constants, each assigned a type, and a collection of equations. This is analogous to a first-order theory, except that all the axioms are just equations.

Higher-order logic (HOL) is a theory in STLC with:

• primitive types $\mathtt{nat}$ and $\mathtt{bool}$
• constants $0 : \mathtt{nat}$, $\mathtt{succ} : \mathtt{nat}$, for each type $\tau$ a constant $\mathtt{rec}_\tau : \tau \to (\tau \to \tau) \to \mathtt{nat} \to \tau$
• constants $\mathtt{false} : \mathtt{bool}$, $\mathtt{true} : \mathtt{bool}$, and for each type $\tau$ a constant $\mathtt{cond} : \tau \to \tau \to \mathtt{bool} \to \tau$
• for each type $\tau$, a constant $\forall_\tau : (\tau \to \mathtt{bool}) \to \mathtt{bool}$.
• a bunch of equations collectively stating that $\mathtt{nat}$ is the natural numbers object
• a bunch of equations collectively stating that $\mathtt{bool}$ is a Boolean algebra and that $\forall_\tau$ is the universal quantifier (to get these, axiomatize $\forall_\tau$ as the right adjoint to weakening, using the fact that logical entailment in a Boolean algebra is expressible with equations).

Because we are still within the realm of STLC, the appropriate categorical models are still the cartesian closed categories (CCC). A model of an STLC theory is a CCC $\mathcal{C}$ with an interpretation of the primitive types and constants that validate the axioms.

The above formalism describes a logic in which the statement that some proposition $p : \mathtt{bool}$ holds is expressed by the equation $p = \mathtt{true}$. However, some bits and pieces are still lacking. For example, we might be interested in stating that $\mathtt{bool}$ is a subobject classifier, but for that we need to extend the type system to new type formers that involve terms. When we do so, we end up with a formulation of the internal language of elementary toposes, see section XXXIII.3 of Lambek & Scott's textbook, and note the powerset operator $P$ axiomatize therein. An important detail is that the powerset constructor $\{ x : A \mid \phi(x) \}$ does not allow parameters in $\phi$, so we are still in the realm of simple types (as opposed to dependent types).

Once we complete HOL with the powerset operator we obtain a mild extension of the simply typed $\lambda$-calculus that is precisely the internal language of elementary toposes, i.e., semantics in elementary toposes is sound and complete for this version of HOL (and since we are using boolean algebra we need to pass to boolean toposes, or else axiomatize Heyting algebras).

Neel mentioned triposes. In my view they are a very powerful tool which allows us to construct elementary toposes. However, the semantics naturally happens in the elementary toposes. For further reading I recommend Lambek & Scott.

Answer 2

The structure you want is due to Andy Pitts, and is called a tripos. It extends the notion of hyperdoctrine, which gives a categorical model for first-order logic, with enough structure to model higher-order logic.

However, much more of the work in this part of categorical logic focuses on toposes instead of triposes, which are just a little bit more expressive than HOL (basically you get to form sets by comprehension, too, giving a model of set theory with bounded quantifiers).

References:

• Andrew M. Pitts, The Theory of Triposes
• Andrew M. Pitts, Tripos theory in retrospect