<p>The distinction is this: if STLC is taken as a primitive language at the <strong>type-level</strong> adding constructors and a small number of axioms is sufficient to give you the full expressive power of HOL.</p>

<p>Taking $\iota$ as the base type of numbers ans $\omicron$ as the base type of propositions, you can add the constants
$$ \forall_\tau:(\tau\rightarrow \omicron)\rightarrow \omicron\quad \supset:\omicron\rightarrow\omicron\rightarrow \omicron$$</p>

<p>where $\tau$ is an arbitrary type (so one $\forall$ constant for each type). One possible set of axioms:</p>

<p>$$ \frac{\phi(x)}{\forall_\tau(\lambda x.\phi(x))}\mbox{$x:\tau$ not free in the hypotheses}$$</p>

<p>$$ \frac{\Large{\substack{[\psi]\\ \\ .\\ .\\ .\\ \\ \phi}}}{\psi\supset \phi}$$</p>

<p>where $[\psi]$ means that the hypothesis $\psi$ is <em>discharged</em>. Interesting fact: the other connectives $\exists_\tau, \vee$... can be derived from just those 2.</p>

<p>The subtlety is distinguishing between $\lambda$-terms as a way to represent proofs, as predicated by the Curry-Howard-de Bruijn (Martin-Löf) correspondence, or as a way to represent the terms you reason upon. The two views are not incompatible, of course.</p>

<p>In particular there is a typed $\lambda$-calculus that faithfully represents HOL (minus various axioms of course). This happens to be a sub-system of the <a href="http://en.wikipedia.org/wiki/Calculus_of_constructions">Calculus of Constructions</a>, and is described in detail by Geuvers in <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.3947"><em>The Calculus of Constructions and Higher Order Logic</em></a>. He also details the differences between the two (the CoC is not a conservative extension of HOL).</p>

CC BY-SA 3.0
2014-11-07T18:48:20.610Z
I forgot to note: you can avoid adding $\forall_\tau$ and $\supset$ if you add $=_\tau :\tau\rightarrow\tau\rightarrow\omicron$ along with some clever axioms, which is what Thomas was suggesting.
cody
CC BY-SA 4.0
2019-03-21T20:35:15.200Z
What are those clever axioms, please? I guess this has to do with providing a way to prove the equality … Also, do you know a name to explicitly distinguish the levels of HOL extensions? (with equality, then with polymorphic type, then with dependant types).
Hibou57
CC BY-SA 4.0
2019-03-21T20:41:09.703Z
@Hibou57 the axioms are outlined in the excellent article [The Seven Virtues of Simple Type Theory](https://www.sciencedirect.com/science/article/pii/S157086830700081X). I don't know that there are explicit names to distinguish different extensions of STT, other than the ones you used.
cody
CC BY-SA 3.0
2014-11-07T15:42:52.280Z
2014-11-07T15:42:52.280Z
cody
<p>What is the relation between simply typed lambda calculus and higher order logic?</p>

<p>Under Curry-Howard it seems that simply typed lambda calculus corresponds to propositional logic. How is it related to higher order logic? According to this tutorial by Geuvers: <a href="http://typessummerschool07.cs.unibo.it/courses/geuvers-1.pdf">http://typessummerschool07.cs.unibo.it/courses/geuvers-1.pdf</a> the language of HOL seems to be STT. Shouldn't it be PROP? What does that mean?</p>

<p>Did Church have in mind HOL when defined STT?</p>

CC BY-SA 3.0
2014-11-06T23:57:23.163Z
Yes, Church did have HOL in mind. The trick to get HOL from STT is to use *equality*, in addition to function application and function abstraction. Then you can write $(\forall x:\alpha.A_*)$ as $(\lambda x:\alpha.A_*)=(\lambda x:\alpha.\top)$, among others. I like "The Seven Virtues of Simple Type Theory" as an introduction to STT, which addresses this sort of questions. Maybe I should write an answer...
Thomas Klimpel
CC BY-SA 3.0
2014-11-07T00:30:18.373Z
So, when talking about Curry-Howard, what would be the correct logic equivalent to STT? HOL or PROP?
lambda2
CC BY-SA 3.0
2014-11-07T00:41:51.453Z
With respect to Curry-Howard, it don't think it will be HOL. Maybe it's the multiplicative fragment of intuitionistic PROP, i.e. intuitionistic PROP without "or". But that was for CCC (cartesian closed category), and I'm a bit tired at the moment. Lambda will probably be translated as "implication", which was the "exponential" in CCC. The "product" from CCC was "and", so you would need a "pair" in STT for that. And "or" would be a "sum" type in STT then, i.e. a disjoint union, maybe an if "a" then "b" else "c" does that.
Thomas Klimpel
CC BY-SA 3.0
2014-11-07T00:49:22.600Z
I think I am confusing something (or everything). If STT ~= PROP (via Curry-Howard), and STT is also HOL, then I can use PROP in some sense to have HOL?
lambda2
CC BY-SA 3.0
2014-11-07T01:07:37.667Z
As I said, you use *equality* to get HOL. For STT ~= PROP (via Curry-Howard), you are not allowed to use *equality* in STT. And think about it, *equality* is simply undecidable, so it has to increase the expressive power if you allow it.
Thomas Klimpel
CC BY-SA 3.0
2014-11-07T15:10:27.263Z
@ThomasKlimpel: you should turn your comments into an answer.
cody
<lo.logic><typed-lambda-calculus><curry-howard>
Simply typed lambda calculus and higher order logic
lambda2
# Simply typed lambda calculus and higher order logic

(Asked by: username_0 on 2014-11-06)

What is the relation between simply typed lambda calculus and higher order logic?

Under Curry-Howard it seems that simply typed lambda calculus corresponds to propositional logic. How is it related to higher order logic? According to this tutorial by Geuvers: <http://typessummerschool07.cs.unibo.it/courses/geuvers-1.pdf> the language of HOL seems to be STT. Shouldn't it be PROP? What does that mean?

Did Church have in mind HOL when defined STT?

**Tags:** lo.logic, typed-lambda-calculus, curry-howard

> **Comments:**
> **username_1**: Yes, Church did have HOL in mind. The trick to get HOL from STT is to use *equality*, in addition to function application and function abstraction. Then you can write $(\forall x:\alpha.A_*)$ as $(\lambda x:\alpha.A_*)=(\lambda x:\alpha.\top)$, among others. I like "The Seven Virtues of Simple Type Theory" as an introduction to STT, which addresses this sort of questions. Maybe I should write an answer...  
> **username_0**: So, when talking about Curry-Howard, what would be the correct logic equivalent to STT? HOL or PROP?  
> **username_1**: With respect to Curry-Howard, it don't think it will be HOL. Maybe it's the multiplicative fragment of intuitionistic PROP, i.e. intuitionistic PROP without "or". But that was for CCC (cartesian closed category), and I'm a bit tired at the moment. Lambda will probably be translated as "implication", which was the "exponential" in CCC. The "product" from CCC was "and", so you would need a "pair" in STT for that. And "or" would be a "sum" type in STT then, i.e. a disjoint union, maybe an if "a" then "b" else "c" does that.  
> **username_0**: I think I am confusing something (or everything). If STT ~= PROP (via Curry-Howard), and STT is also HOL, then I can use PROP in some sense to have HOL?  
> **username_1**: As I said, you use *equality* to get HOL. For STT ~= PROP (via Curry-Howard), you are not allowed to use *equality* in STT. And think about it, *equality* is simply undecidable, so it has to increase the expressive power if you allow it.  
> **username_2**: @ThomasKlimpel: you should turn your comments into an answer.  

---

## 1 answers

### Answer by username_2 on 2014-11-07. Score: 11 | Accepted answer

The distinction is this: if STLC is taken as a primitive language at the **type-level** adding constructors and a small number of axioms is sufficient to give you the full expressive power of HOL.

Taking $\iota$ as the base type of numbers ans $\omicron$ as the base type of propositions, you can add the constants
$$ \forall\_\tau:(\tau\rightarrow \omicron)\rightarrow \omicron\quad \supset:\omicron\rightarrow\omicron\rightarrow \omicron$$

where $\tau$ is an arbitrary type (so one $\forall$ constant for each type). One possible set of axioms:

$$ \frac{\phi(x)}{\forall\_\tau(\lambda x.\phi(x))}\mbox{$x:\tau$ not free in the hypotheses}$$

$$ \frac{\Large{\substack{[\psi]\\ \\ .\\ .\\ .\\ \\ \phi}}}{\psi\supset \phi}$$

where $[\psi]$ means that the hypothesis $\psi$ is *discharged*. Interesting fact: the other connectives $\exists\_\tau, \vee$... can be derived from just those 2.

The subtlety is distinguishing between $\lambda$-terms as a way to represent proofs, as predicated by the Curry-Howard-de Bruijn (Martin-Löf) correspondence, or as a way to represent the terms you reason upon. The two views are not incompatible, of course.

In particular there is a typed $\lambda$-calculus that faithfully represents HOL (minus various axioms of course). This happens to be a sub-system of the [Calculus of Constructions](http://en.wikipedia.org/wiki/Calculus_of_constructions), and is described in detail by Geuvers in [*The Calculus of Constructions and Higher Order Logic*](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.3947). He also details the differences between the two (the CoC is not a conservative extension of HOL).

> **Comments:**
> **username_2**: I forgot to note: you can avoid adding $\forall_\tau$ and $\supset$ if you add $=_\tau :\tau\rightarrow\tau\rightarrow\omicron$ along with some clever axioms, which is what Thomas was suggesting.  
> **username_3**: What are those clever axioms, please? I guess this has to do with providing a way to prove the equality … Also, do you know a name to explicitly distinguish the levels of HOL extensions? (with equality, then with polymorphic type, then with dependant types).  
> **username_2**: @username_3 the axioms are outlined in the excellent article [The Seven Virtues of Simple Type Theory](https://www.sciencedirect.com/science/article/pii/S157086830700081X). I don't know that there are explicit names to distinguish different extensions of STT, other than the ones you used.  

---

