We now explore the fundamental duality of Binary Logic, which also generalizes to Matrix Logics and Active Logics.

<aside> 💡 Or is dual to And

</aside>

A proof from (X or Y) to P is equivalent to A proof from X to P, and a proof from Y to P.

In symbols,

$$ (X+Y)\to P \\ \;\;\;\;\sim \\ \;\;\;\;(X\to P)\\ \times\; (Y\to P) $$

If you have a program that inputs either X or Y and outputs P, then you have a program from X to P, and a program from Y to P.

This duality is extremely useful, because:

<aside> <img src="https://prod-files-secure.s3.us-west-2.amazonaws.com/4f2cadbd-854d-4cf8-a906-ade20a1e2895/b614169f-b7a0-4cea-9221-e0de3848715a/yin-yang.png" alt="https://prod-files-secure.s3.us-west-2.amazonaws.com/4f2cadbd-854d-4cf8-a906-ade20a1e2895/b614169f-b7a0-4cea-9221-e0de3848715a/yin-yang.png" width="40px" /> Composition is Some, which is indexed Or, Transformation is All, which is indexed And.

</aside>

Relation composition is defined by Some:

$$ (R\circ S)(\mathrm{a,c}) = \mathsf{\Sigma} \mathrm{b:B}.\; R(\mathrm{a,b}) \times S(\mathrm{b,c}) $$

Relation inference is defined by All:

$$ [P\Rightarrow Q] \;=\;\mathsf{\Pi}\, \mathrm{x:X,y:Y} .\; P(\mathrm{x,y})\to Q(\mathrm{x,y}) $$