14
$\begingroup$

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?

Improve this question
$\endgroup$
6
  • 6
    $\begingroup$ 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... $\endgroup$
    – Thomas Klimpel
    Nov 6, 2014 at 23:57
  • $\begingroup$ So, when talking about Curry-Howard, what would be the correct logic equivalent to STT? HOL or PROP? $\endgroup$
    – lambda2
    Nov 7, 2014 at 0:30
  • $\begingroup$ 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. $\endgroup$
    – Thomas Klimpel
    Nov 7, 2014 at 0:41
  • $\begingroup$ 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? $\endgroup$
    – lambda2
    Nov 7, 2014 at 0:49
  • 1
    $\begingroup$ @ThomasKlimpel: you should turn your comments into an answer. $\endgroup$
    – cody
    Nov 7, 2014 at 15:10

1 Answer 1

Reset to default
11
$\begingroup$

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, and is described in detail by Geuvers in The Calculus of Constructions and Higher Order Logic. He also details the differences between the two (the CoC is not a conservative extension of HOL).

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ 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. $\endgroup$
    – cody
    Nov 7, 2014 at 18:48
  • $\begingroup$ 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). $\endgroup$
    – Hibou57
    Mar 21, 2019 at 20:35
  • 2
    $\begingroup$ @Hibou57 the axioms are outlined in the excellent article The Seven Virtues of Simple Type Theory. I don't know that there are explicit names to distinguish different extensions of STT, other than the ones you used. $\endgroup$
    – cody
    Mar 21, 2019 at 20:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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