Logical disjunction ($\vee$)

The disjunction $A\vee B$ holds when at least one of $A$ and $B$ holds. Constructively, a proof records which disjunct holds and provides its proof.

A logic gate computing inclusive logical disjunction: its output is one exactly when at least one input is one.