<p>I suspect someone is going to come along with a deep category-theoretic reason for the connection, but in the meantime, here is my insight.</p>
<p>Both logic and programming with functions are built around the notion of <em>hypotheticals</em>. The proposition <span class="math-container">$A \to B$</span> says &quot;If I had an <span class="math-container">$A$</span>, I could prove <span class="math-container">$B$</span>.&quot; A function of type <span class="math-container">$A \to B$</span> says &quot;If I had a value of type <span class="math-container">$A$</span>, I could compute a value of type <span class="math-container">$B$</span>. So these logics/languages are really systems for hypothetical reasoning, which we need for both programming and proving.</p>
<p>Whether we say &quot;prove&quot; or &quot;compute&quot; really just depends on whether we only care about the <em>existence</em> of an <span class="math-container">$B$</span>, or whether we care about <em>which</em> <span class="math-container">$B$</span> we get. But this isn't a change in the system, it's just a change in its use.</p>
<p>In some sense, the Curry-Howard isomorphism isn't an isomorphism at all, and some people prefer the word &quot;correspondence&quot;. But depending on your view, it's not &quot;two things that are isomorphic&quot; but &quot;two different views of the same thing.&quot; You don't have to view it as there being two systems, logic and programming, that are separate but connected.</p>
<p>Instead, I view it as &quot;here is a single system for reasoning about abstraction and hypotheticals, and it turns out we can view this system as either a logic or as a programming language.&quot; It's not a connection between two things, but two uses of a single thing.</p>

CC BY-SA 4.0
2021-11-10T19:15:15.417Z
I think it's also worth noting that Church's earliest papers on lambda calculus were attempting to create a formal system for logic, similar to a modern "logical framework." Lambda terms for computation was (publication-wise at least) slightly later.
Dan Doel
CC BY-SA 4.0
2021-11-12T19:14:05.017Z
@DanDoel it turns out "a calculus of first-class substitutions" is a really useful idea!
cody
CC BY-SA 4.0
2021-11-10T17:56:31.853Z
2021-11-10T17:56:31.853Z
Joey Eremondi
<p>Someone wanted a deep category-theoretic insight?</p>
<blockquote>
<p><em>A Heyting algebra is a cartesian-closed category.</em></p>
</blockquote>

CC BY-SA 4.0
2021-11-12T05:50:30.380Z
I was guessing you would say “a topology is a Heyting algebra!”
Neel Krishnaswami
CC BY-SA 4.0
2021-11-13T19:59:31.283Z
What has topology got to do with $\lambda$-calculus?
Andrej Bauer
CC BY-SA 4.0
2021-11-15T09:51:26.017Z
(a) the topology via logic view, where termination/nontermination gets modelled by the Sierpinksi space, and computable functions are modelled by continuous ones,
Neel Krishnaswami
CC BY-SA 4.0
2021-11-15T09:55:16.953Z
(b) the ability to do finite observations of data structures corresponds to be able to answer questions in geometric logic about them. E.g, see Balat et al, POPL 2004, *Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums*, which formed a Grothendieck topology using the branches of pattern matches.
Neel Krishnaswami
CC BY-SA 4.0
2021-11-15T10:47:09.363Z
Ok, but how does this explain why the $\lambda$-calculus and propositional calculus are related? For instance, what do question of termination have to do with anything when we explain the Curry-Howard correspondence?
Andrej Bauer
CC BY-SA 4.0
2021-11-15T10:47:50.007Z
There is a relation between topology and logic, namely that the Sierpinski space classifies semidecidable/open propositions. It sounds to me like that's what you're talking about.
Andrej Bauer
CC BY-SA 4.0
2021-11-11T14:58:54.880Z
2021-11-11T14:58:54.880Z
Andrej Bauer
<p>The Curry-Howard isomorphism is the correspondence between type systems (like for the simply typed lambda calculus) and proof systems (like natural deduction). More precisely, types resemble propositions, terms resemble proofs, reduction resembles cut elimination etc.</p>
<p>The isomorphism becomes obvious because there is a 1-to-1 correspondence between the inference rules of Curry typing and the inference rules of predicate logic ND systems, for example.</p>
<p>However, what is not obvious (to me) is <em>why</em> this happens. Is there a deeper reason that proofs and typing are just two facets of the same system?</p>
<p>Merely noting that this is possible because the basic definitions are isomorphic is not really satisfactory, because this just shifts the question towards asking why the definitions of these systems end up isomorphic.</p>

<type-theory><curry-howard><natural-deduction>
Why is the Curry-Howard isomorphism?
JoJoModding
# Why is the Curry-Howard isomorphism?

(Asked by: username_0 on 2021-11-10)

The Curry-Howard isomorphism is the correspondence between type systems (like for the simply typed lambda calculus) and proof systems (like natural deduction). More precisely, types resemble propositions, terms resemble proofs, reduction resembles cut elimination etc.

The isomorphism becomes obvious because there is a 1-to-1 correspondence between the inference rules of Curry typing and the inference rules of predicate logic ND systems, for example.

However, what is not obvious (to me) is *why* this happens. Is there a deeper reason that proofs and typing are just two facets of the same system?

Merely noting that this is possible because the basic definitions are isomorphic is not really satisfactory, because this just shifts the question towards asking why the definitions of these systems end up isomorphic.

**Tags:** type-theory, curry-howard, natural-deduction

---

## 2 answers

### Answer by username_1 on 2021-11-10. Score: 14

I suspect someone is going to come along with a deep category-theoretic reason for the connection, but in the meantime, here is my insight.

Both logic and programming with functions are built around the notion of *hypotheticals*. The proposition $A \to B$ says "If I had an $A$, I could prove $B$." A function of type $A \to B$ says "If I had a value of type $A$, I could compute a value of type $B$. So these logics/languages are really systems for hypothetical reasoning, which we need for both programming and proving.

Whether we say "prove" or "compute" really just depends on whether we only care about the *existence* of an $B$, or whether we care about *which* $B$ we get. But this isn't a change in the system, it's just a change in its use.

In some sense, the Curry-Howard isomorphism isn't an isomorphism at all, and some people prefer the word "correspondence". But depending on your view, it's not "two things that are isomorphic" but "two different views of the same thing." You don't have to view it as there being two systems, logic and programming, that are separate but connected.

Instead, I view it as "here is a single system for reasoning about abstraction and hypotheticals, and it turns out we can view this system as either a logic or as a programming language." It's not a connection between two things, but two uses of a single thing.

> **Comments:**
> **username_2**: I think it's also worth noting that Church's earliest papers on lambda calculus were attempting to create a formal system for logic, similar to a modern "logical framework." Lambda terms for computation was (publication-wise at least) slightly later.  
> **username_3**: @DanDoel it turns out "a calculus of first-class substitutions" is a really useful idea!  

---

### Answer by username_4 on 2021-11-11. Score: 7

Someone wanted a deep category-theoretic insight?

> *A Heyting algebra is a cartesian-closed category.*

> **Comments:**
> **username_5**: I was guessing you would say “a topology is a Heyting algebra!”  
> **username_4**: What has topology got to do with $\lambda$-calculus?  
> **username_5**: (a) the topology via logic view, where termination/nontermination gets modelled by the Sierpinksi space, and computable functions are modelled by continuous ones,  
> **username_5**: (b) the ability to do finite observations of data structures corresponds to be able to answer questions in geometric logic about them. E.g, see Balat et al, POPL 2004, *Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums*, which formed a Grothendieck topology using the branches of pattern matches.  
> **username_4**: Ok, but how does this explain why the $\lambda$-calculus and propositional calculus are related? For instance, what do question of termination have to do with anything when we explain the Curry-Howard correspondence?  
> **username_4**: There is a relation between topology and logic, namely that the Sierpinski space classifies semidecidable/open propositions. It sounds to me like that's what you're talking about.  

---

