3
$\begingroup$

Intuitionistic logic(s) are usually defined in a purely synthetic way, with their own deduction rules different from classical logic, but they also have semantic interpretations.

One of them, more known in mathematical logic, is Kripke semantics, originated in modal logic, in which a formula is valid iff it holds in all Kripke frames. Another interpretation, more known in computer science, is the Curry-Howard isomorphism, in which a proposition is interpretated as type in a suitable system and a proposition is valid iff there is a program of that type.

My question is: Is there any relation between these two interpretations? They are certainly equivalent, but merely concluding that from the two previous equivalences don't give any insight into a probably much deeper connection.

EDIT: Should I have posted this question in the Theoretical Computer Science Stack Exchange?

$\endgroup$
5
  • $\begingroup$ Why do you say that they are "certainly equivalent", and what does that mean, precisely? $\endgroup$ Jun 17, 2023 at 21:29
  • $\begingroup$ We know that p is intuitionistically valid iff p is valid in all kripke frame and that p is intuitionistically valid iff the corresponding type is inhabited, thus p is valid in all kripke frame iff the corresponding type is inhabited. Thats all I meant by equivalent $\endgroup$
    – manu fava
    Jun 17, 2023 at 22:11
  • $\begingroup$ What logic are you talking about? Propositional, predicate? It matters. $\endgroup$ Jun 17, 2023 at 22:46
  • $\begingroup$ I mean, I could pose the question for both of them. For propositional you would use simply-typed lambda calculus and simple kripke frames, and for predicative you would use some system with dependent types and kripke frames with universal quantifiers. But for simplicity Im more interested in the propositional case. $\endgroup$
    – manu fava
    Jun 17, 2023 at 23:14
  • $\begingroup$ By the way, congratulations for your fantastic essay introducing constructive mathematics. Its one of the reason that got me so interested in intuitionism and type theory! $\endgroup$
    – manu fava
    Jun 17, 2023 at 23:17

2 Answers 2

3
$\begingroup$

Both Kripke semantics and propositions-as-types interpretation are sound and complete for the intuitionistic propositional calculus. In this sense they are equivalent.

However, there are formulas in intuitionistic first-order logic (IHOL) which are valid under propositions-as-types but are not intuitionistically provable. See Remark 6.6. of Propositions as [Types], where the following formula is given: $$ (\forall x . \exists y . R(x, y)) \Rightarrow (\forall x, x' . \exists y, y' . R(x,y) \land R(x',y') \land (x = x' \Rightarrow y = y')). $$ This is not provable intuitionistically, but it can be inhabited under propositions-as-types interpretation. Because Kripke semantics is complete for IHOL, the above formula provides a distinction between the two setups.

$\endgroup$
2
$\begingroup$

For propositional logic, you're probably right. As far as quantifier logic goes: the Curry-Howard correspondence never included quantifiers and there isn't really any consensus or standard treatment for such an extension.

I discuss the matter in greater depth here Curry-Howard correspondence in CIC/propositional logic?, so I won't repeat the points here, except to reiterate the Dana Scott reference and add in a few more links.

As I noted there, the approach, arising from de Bruijn (particularly from AutoMath) and Martin-Löf (along with the rest of the Lambda Cube), deals with higher-order logic and its corresponding type theory, and is sometimes confused with Curry-Howard, but is actually an independent line of development and is not actually compatible with Curry-Howard.

To handle quantifiers, in the spirit of Curry-Howard, would require treating them as infinitary analogues of the $∧$ connective (for $∀$) and the $∨$ (for $∃$). That falls in line with the treatment given by Dana Scott The Algebraic Interpretation of Quantifiers: Intuitionistic and Classical, which stays in the confines of first-order logic, and also deals with the modal logic representation (section 10) ... which (as I just noticed) ties into Kripke Semantics (and is also discussed in the paper in section 6).

You may also find this paper Intuitionistic First-Order Logic: Categorical Semantics via the Curry-Howard Isomorphism, on ArXiv, to be of interest. It's laying out a category-theoretic semantics that, as per its abstract, "extends, in a way, the more traditional meanings given by Heyting categories, the topos-theoretic interpretation, and Kripke models". So, that might even be what you're looking for. I haven't read it in detail yet, though and am still reading through the Dana Scott link.

$\endgroup$

Your Answer

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

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