## Curry/Howard and Disjunction

Whilst tralling for Propositions-as-Types references a question arose about the difference between disjunction in propositional logic calculi and sum-types in PLs.

To the best of my knowledge Curry/Howard makes a connection between the 2 concepts even though disjunction is an inclusive-or and sum-types are exclusive, e.g.

A v B ~= A | B | A x B

Am I missing something?

Is choice disjunction in CL also exclusive?

## Comment viewing options

### Think of a proof term (ie, a

Think of a proof term (ie, a lambda term) as a witness that you have sufficient evidence to demonstrate that the proposition (ie, the type) is provable.

In this sense, you can make an A + B if you've got an e1:A, an e2:B, or both. In the case where you've got evidence for both A and B on hand, you can prove A + B two different ways, either with inl e1 or inr e2, whichever you like.

### Both sum type former and logical disjunction are inclusive or

The sum type described in CH is inclusive sum.