<p>It seems to me there isn't an agreement about what &quot;HOL&quot; 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 <span class="math-container">$\lambda$</span>-calculus. To give the question some clarity, allow me to spell out my understanding of what such a formalism comprises.</p>
<p>Recall the notion of a <em>theory</em> 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 <span class="math-container">$\lambda$</span>-calculus.</p>
<p>A <em>theory</em> 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.</p>
<p>Higher-order logic (HOL) is a theory in STLC with:</p>
<ul>
<li>primitive types <span class="math-container">$\mathtt{nat}$</span> and <span class="math-container">$\mathtt{bool}$</span></li>
<li>constants <span class="math-container">$0 : \mathtt{nat}$</span>, <span class="math-container">$\mathtt{succ} : \mathtt{nat}$</span>, for each type <span class="math-container">$\tau$</span> a constant <span class="math-container">$\mathtt{rec}_\tau : \tau \to (\tau \to \tau) \to \mathtt{nat} \to \tau$</span></li>
<li>constants <span class="math-container">$\mathtt{false} : \mathtt{bool}$</span>, <span class="math-container">$\mathtt{true} : \mathtt{bool}$</span>, and for each type <span class="math-container">$\tau$</span> a constant <span class="math-container">$\mathtt{cond} : \tau \to \tau \to \mathtt{bool} \to \tau$</span></li>
<li>for each type <span class="math-container">$\tau$</span>, a constant <span class="math-container">$\forall_\tau : (\tau \to \mathtt{bool}) \to \mathtt{bool}$</span>.</li>
<li>a bunch of equations collectively stating that <span class="math-container">$\mathtt{nat}$</span> is the natural numbers object</li>
<li>a bunch of equations collectively stating that <span class="math-container">$\mathtt{bool}$</span> is a Boolean algebra and that <span class="math-container">$\forall_\tau$</span> is the universal quantifier (to get these, axiomatize <span class="math-container">$\forall_\tau$</span> as the right adjoint to weakening, using the fact that logical entailment in a Boolean algebra is expressible with equations).</li>
</ul>
<p>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 <span class="math-container">$\mathcal{C}$</span> with an interpretation of the primitive types and constants that validate the axioms.</p>
<p>The above formalism describes a logic in which the statement that some proposition <span class="math-container">$p : \mathtt{bool}$</span> holds is expressed by the equation <span class="math-container">$p = \mathtt{true}$</span>. However, some bits and pieces are still lacking. For example, we might be interested in stating that <span class="math-container">$\mathtt{bool}$</span> 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 <a href="https://books.google.si/books?id=6PY_emBeGjUC&amp;lpg=PP1&amp;dq=scott%20lambek%20higher-order&amp;pg=PA133#v=onepage&amp;q&amp;f=false" rel="noreferrer">section XXXIII.3</a> of Lambek &amp; Scott's textbook, and note the powerset operator <span class="math-container">$P$</span> axiomatize therein. An important detail is that the powerset constructor <span class="math-container">$\{ x  : A \mid \phi(x) \}$</span> does <em>not</em> allow parameters in <span class="math-container">$\phi$</span>, so we are still in the realm of simple types (as opposed to dependent types).</p>
<p>Once we complete HOL with the powerset operator we obtain a mild extension of the simply typed <span class="math-container">$\lambda$</span>-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 <em>boolean</em> algebra we need to pass to <em>boolean</em> toposes, or else axiomatize Heyting algebras).</p>
<p>Neel mentioned triposes. In my view they are a very powerful <em>tool</em> which allows us to construct elementary toposes. However, the semantics naturally happens in the elementary toposes. For further reading I recommend Lambek &amp; Scott.</p>

CC BY-SA 4.0
2024-09-29T13:43:44.977Z
Thanks for this great answer!

I think that it's safe to say that I'm just getting started with this stuff. I was wondering if you could give a slightly more elaborate example of 'the missing bits and pieces' like the subobject classifier (which I don't exactly know what it means..)? Do you mean that φ == `Bool is a subobject classifier` would be a wff? 

On a related note, could we state / reason about statements like that (`Bool is a subobject classifier`) in ZFC?
Suraaj K S
CC BY-SA 4.0
2024-09-29T15:18:44.190Z
Another thing that seems a little bit different for me is this: Here, it doesn't seem to be the case that types are propositions. Here, propositions seem to be themselves *terms* of type `bool`. Furthermore, it seems like the typical proofs are programs idea also does not apply here..
Suraaj K S
CC BY-SA 4.0
2024-09-29T16:17:29.533Z
Correct, propositions are *not* types, they are elements of the type `bool`. It is  called a *logic*, after all.
Andrej Bauer
CC BY-SA 4.0
2024-09-29T16:24:02.720Z
I wouldn't have thought that you could include something like "for all types $\tau$" in a *theory* of STLC.  I usually think of a theory as given by specifying some base types, some function symbols, and some axioms.  I suppose you could first specify the base types, then observe all the syntactic types that were generated by those, and add a function symbol and axioms for each of those.  But I don't think that would have the desired effect, e.g. in a CCC that's a model of the theory it wouldn't ensure that you have a $\forall$ operator for each *object*, only for those in the image of syntax.
Mike Shulman
CC BY-SA 4.0
2024-09-29T16:33:36.273Z
I don't quite understand you. Are you discussing a possible extension of HOL? There *are* quantifiers $\forall_A : (A \to \mathsf{bool}) \to \mathsf{bool}$, one for each type $A$, but you seem to have something else in mind, possibly System F-style quantifiers. (Also note that a weak kind of "for all types" can be modeled schematically with type meta-variables.)
Andrej Bauer
CC BY-SA 4.0
2024-09-29T18:02:03.370Z
@AndrejBauer, thanks for your response. In that case, would it be safe to say that 'the Curry-Howard correspondence' does not make sense when we talk about Isabelle/HOL (because it is a logic, and not a type theory)?
Suraaj K S
CC BY-SA 4.0
2024-09-29T19:18:04.657Z
Yes, I think it is fair to say that HOL is not a Curry-Howard correspondence. Or to be more precise, we *can* carry out a Curry-Howard-style correspondence between logic and HOL, but we will only be able to do so for the *propositional calculus*. For predicate calculus we need dependent types.
Andrej Bauer
CC BY-SA 4.0
2020-08-01T08:09:40.490Z
2020-08-01T08:23:36.393Z
2020-08-01T08:23:36.393Z
Andrej Bauer
<p>The structure you want is due to Andy Pitts, and is called a <a href="https://ncatlab.org/nlab/show/tripos" rel="noreferrer"><em>tripos</em></a>. It extends the notion of <a href="https://ncatlab.org/nlab/show/hyperdoctrine" rel="noreferrer"><em>hyperdoctrine</em></a>, which gives a categorical model for first-order logic, with enough structure to model higher-order logic.</p>
<p>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).</p>
<p>References:</p>
<ul>
<li>Andrew M. Pitts, <a href="http://www.cl.cam.ac.uk/%7Eamp12/papers/thet/thet.pdf" rel="noreferrer"><em>The Theory of Triposes</em></a></li>
<li>Andrew M. Pitts, <a href="http://www.cl.cam.ac.uk/%7Eamp12/papers/tritr/tritr.pdf" rel="noreferrer"><em>Tripos theory in retrospect</em></a></li>
</ul>

CC BY-SA 4.0
2020-07-31T13:02:14.407Z
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"
user1868607
CC BY-SA 4.0
2020-07-31T19:56:18.047Z
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?)
Andrej Bauer
CC BY-SA 4.0
2020-07-31T22:10:50.707Z
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?
Neel Krishnaswami
CC BY-SA 4.0
2020-08-01T07:51:11.547Z
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.
Andrej Bauer
CC BY-SA 4.0
2020-08-01T08:12:33.703Z
There, I spelled out my understanding of the matter.
Andrej Bauer
CC BY-SA 4.0
2020-07-31T12:30:08.417Z
2020-07-31T12:30:08.417Z
Neel Krishnaswami
<p>From <a href="https://cstheory.stackexchange.com/questions/27367/simply-typed-lambda-calculus-and-higher-order-logic">Simply typed lambda calculus and higher order logic</a>, I get the impression that HOL is STLC + equality + equality axioms. I was wondering if there is a particular kind of category modelling this.</p>

<lo.logic><lambda-calculus><ct.category-theory>
Categorical equivalent of higher order logic
user1868607
# Categorical equivalent of higher order logic

(Asked by: username_0 on 2020-07-31)

From [Simply typed lambda calculus and higher order logic](https://cstheory.stackexchange.com/questions/27367/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.

**Tags:** lo.logic, lambda-calculus, ct.category-theory


---

## 2 answers

### Answer by username_1 on 2020-08-01. Score: 8 | Accepted answer

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](https://books.google.si/books?id=6PY_emBeGjUC&lpg=PP1&dq=scott%20lambek%20higher-order&pg=PA133#v=onepage&q&f=false) 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.

> **Comments:**
> **username_2**: Thanks for this great answer!  I think that it's safe to say that I'm just getting started with this stuff. I was wondering if you could give a slightly more elaborate example of 'the missing bits and pieces' like the subobject classifier (which I don't exactly know what it means..)? Do you mean that φ == `Bool is a subobject classifier` would be a wff?   On a related note, could we state / reason about statements like that (`Bool is a subobject classifier`) in ZFC?  
> **username_2**: Another thing that seems a little bit different for me is this: Here, it doesn't seem to be the case that types are propositions. Here, propositions seem to be themselves *terms* of type `bool`. Furthermore, it seems like the typical proofs are programs idea also does not apply here..  
> **username_1**: Correct, propositions are *not* types, they are elements of the type `bool`. It is  called a *logic*, after all.  
> **username_3**: I wouldn't have thought that you could include something like "for all types $\tau$" in a *theory* of STLC.  I usually think of a theory as given by specifying some base types, some function symbols, and some axioms.  I suppose you could first specify the base types, then observe all the syntactic types that were generated by those, and add a function symbol and axioms for each of those.  But I don't think that would have the desired effect, e.g. in a CCC that's a model of the theory it wouldn't ensure that you have a $\forall$ operator for each *object*, only for those in the image of syntax.  
> **username_1**: I don't quite understand you. Are you discussing a possible extension of HOL? There *are* quantifiers $\forall_A : (A \to \mathsf{bool}) \to \mathsf{bool}$, one for each type $A$, but you seem to have something else in mind, possibly System F-style quantifiers. (Also note that a weak kind of "for all types" can be modeled schematically with type meta-variables.)  
> **username_2**: @AndrejBauer, thanks for your response. In that case, would it be safe to say that 'the Curry-Howard correspondence' does not make sense when we talk about Isabelle/HOL (because it is a logic, and not a type theory)?  
> **username_1**: Yes, I think it is fair to say that HOL is not a Curry-Howard correspondence. Or to be more precise, we *can* carry out a Curry-Howard-style correspondence between logic and HOL, but we will only be able to do so for the *propositional calculus*. For predicate calculus we need dependent types.  

---

### Answer by username_4 on 2020-07-31. Score: 8

The structure you want is due to Andy Pitts, and is called a [*tripos*](https://ncatlab.org/nlab/show/tripos). It extends the notion of [*hyperdoctrine*](https://ncatlab.org/nlab/show/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*](http://www.cl.cam.ac.uk/%7Eamp12/papers/thet/thet.pdf)
* Andrew M. Pitts, [*Tripos theory in retrospect*](http://www.cl.cam.ac.uk/%7Eamp12/papers/tritr/tritr.pdf)

> **Comments:**
> **username_0**: 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"  
> **username_1**: 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?)  
> **username_4**: 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?  
> **username_1**: 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.  
> **username_1**: There, I spelled out my understanding of the matter.  

---

