# Is sum type a disjoint or more of a multiplexer?

In Wikipedia article on "Sum Type" it is stated that sum type Curry-Howard correspondence is intuitionistic logical disjoint.

But sum type definition states that it is

a data structure used to hold a value that could take on several different, but fixed, types. Only one of the types can be in use at any one time, and a tag field explicitly indicates which one is in use.

whereas in disjunction you can have both values present at the same time.

To me it looks like sum type is more like a multiplexer than a simple "or", that is $$(A\land S) \lor(A \land \lnot S)$$, specially because its eliminator acts like a case statement.

I would appreciate if someone can make it clear for me.

• In a disjunction $A \lor B$, both $A$ and $B$ can be true, but to witness a proof of $A \lor B$ you use either $A$ or $B$, but not both. In a sum type $A + B$, you can have terms of both type $A$ and type $B$, but to give a term of type $A + B$, you use either the term of type $A$ or the term of type $B$, but not both. Dec 8, 2021 at 17:43
• @varkor “to witness a proof of A∨B you use either A or B” in intuitionistic logic, yes. But in classical logic, you can use the law of excluded middle and use neither. So in a classical logic proof, you don't have to say that you're using one side of the disjunction or the other. Dec 8, 2021 at 18:57
• @Gilles'SO-stopbeingevil': yes, that is a good point, and a good answer. Dec 8, 2021 at 20:17

In classical logic, yes. But the Curry-Howard correspondence relates basic type theory to intuitionistic logic. And in intuitionistic logic, to speak intuitively, when you know that $$A \vee B$$ is true, you know which one is true.
The idea of intuitionistic logic is that if you can prove a proposition $$P$$, it doesn't mean “$$P$$ is true” (as it does in classical logic), but “I know how to prove $$P$$”. When the proposition is of the form $$A \vee B$$, the way to prove $$A \vee B$$ must either involve a proof of $$A$$ or a proof of $$B$$, plus the information of which side you chose to prove. This is not true in classical logic, which has $$A \vee \neg A$$ as an axiom, which doesn't tell you which of $$A$$ or $$\neg A$$ is true or how you'd prove it. The absence of this axiom, the excluded middle, is the defining feature of intuitionistic logic compared to classical logic.