Disjunction

Definition

Disjunction is a logical connective representing “or”. In classical logic, the disjunction $P\vee Q$ is true if at least one of $P$ or $Q$ is true.

In Type Theory

Under the propositions-as-types interpretation, disjunction corresponds to the Sum Type:

$P\vee Q\equiv P+Q$

A proof of $P\vee Q$ is either a proof of $P$ (via $\text{inl}$) or a proof of $Q$ (via $\text{inr}$).

Properties

• Commutativity: $P\vee Q\equiv Q\vee P$
• Associativity: $(P\vee Q)\vee R\equiv P\vee (Q\vee R)$
• Identity: $P\vee \perp \equiv P$ where $\perp$ is falsity
• Idempotence: $P\vee P\equiv P$

Elimination

To use a disjunction $P\vee Q$ to prove some conclusion $C$, one must provide:

• A proof that $P\to C$
• A proof that $Q\to C$

This corresponds to case analysis on the sum type.

Related Concepts

• Conjunction: The dual connective representing “and”
• Sum Type: The type-theoretic interpretation of disjunction
• Logical Connective: The family of logical operations
• Proposition: What disjunction operates on