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.


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.

| cite | improve this answer | |

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).


| cite | improve this answer | |
  • $\begingroup$ It is difficult to find a text linking explicitely the two. Also, I think there are different versions of HOL so I'm assuming this refers to what I said before: "STLC + equality + equality axioms" $\endgroup$ – Rodrigo Jul 31 at 13:02
  • $\begingroup$ I do not undertand this answer. Why isn't the correct answer: the structure you want is a CCC with a natural numbers object and a Boolean algebra? (HOL doesn't posit that the boolean algebra is the subojbect classifier, does it?) $\endgroup$ – Andrej Bauer Jul 31 at 19:56
  • $\begingroup$ My picture of HOL is that you have sorts as the types of the STLC, including a distinguished type of propositions. You can write terms ranging over any of these sorts, and terms of the prop sort are the predicates. The semantics of logical formulas in context are given by a functor into Heyting/Boolean algebras, and (a) you need the hyperdoctrine machinery to interpret quantifiers, and (b) you need the tripos machinery to smoosh together the semantics of logical connectives and terms of the prop type. Is this wrong? $\endgroup$ – Neel Krishnaswami Jul 31 at 22:10
  • $\begingroup$ In HOL, i.e., the particular formalizations using STLC, no special status is given to propositions. All logic is done equationally in the distinguished boolean algebra, which is just another type of STLC. If I understand you correctly, you are talking about a formalism that has a special judgement form for propositions, and in that case you would indeed need something like a hyperdoctrine, but as far as I know, HOL does not have anything like that. $\endgroup$ – Andrej Bauer Aug 1 at 7:51
  • $\begingroup$ There, I spelled out my understanding of the matter. $\endgroup$ – Andrej Bauer Aug 1 at 8:12

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.