nLab disjunction

Logical disjunction

Logical disjunction

Definitions

In logic, logical disjunction is the join in the poset of truth values.

Assuming that (as in classical logic) the only truth values are true (TT) and false (FF), then the disjunction pqp \vee q of the truth values pp and qq may be defined by a truth table:

ppqqpqp \vee q
TTTTTT
TTFFTT
FFTTTT
FFFFFF

That is, pqp \vee q is true if and only if at least one of pp and qq is true. Disjunction also exists in nearly every non-classical logic.

More generally, if pp and qq are any two relations on the same domain, then we define their disjunction pointwise, thinking of a relation as a function to truth values. If instead we think of a relation as a subset of its domain, then disjunction becomes union.

In natural deduction the inference rules for disjunction are given as

ΓPpropΓQpropΓPQpropΓPpropΓQpropΓ,PtruePQtrueΓPpropΓQpropΓ,QtruePQtrue\frac{\Gamma \vdash P \; \mathrm{prop} \quad \Gamma \vdash Q \; \mathrm{prop}}{\Gamma \vdash P \vee Q \; \mathrm{prop}} \qquad \frac{\Gamma \vdash P \; \mathrm{prop} \quad \Gamma \vdash Q \; \mathrm{prop}}{\Gamma, P \; \mathrm{true} \vdash P \vee Q \; \mathrm{true}} \qquad \frac{\Gamma \vdash P \; \mathrm{prop} \quad \Gamma \vdash Q \; \mathrm{prop}}{\Gamma, Q \; \mathrm{true} \vdash P \vee Q \; \mathrm{true}}
ΓPpropΓQpropΓ,PQtrueRpropΓ,PtrueRtrueΓ,QtrueRtrueΓ,PQtrueRtrue\frac{\Gamma \vdash P \; \mathrm{prop} \quad \Gamma \vdash Q \; \mathrm{prop} \quad \Gamma, P \vee Q \; \mathrm{true} \vdash R \; \mathrm{prop} \quad \Gamma, P \; \mathrm{true} \vdash R \; \mathrm{true} \quad \Gamma, Q \; \mathrm{true} \vdash R \; \mathrm{true}}{\Gamma, P \vee Q \; \mathrm{true} \vdash R \; \mathrm{true}}

Remarks

Disjunction as defined above is sometimes called inclusive disjunction to distinguish it from exclusive disjunction, where exactly one of pp and qq must be true.

In the context of substructural logics such as linear logic, we often have both additive disjunction \oplus and multiplicative disjunction \parr; see the Rules of Inference below for the distinction. In linear logic, additive disjunction is the join under the entailment relation, just like disjunction in classical logic (and intuitionistic logic), while multiplicative disjunction is something different.

Disjunction is de Morgan dual to conjunction.

Like any join, disjunction is an associative operation, so we can take the disjunction of any finite positive whole number of truth values; the disjunction is true if and only if at least one of the various truth values is true. Disjunction also has an identity element, which is the false truth value. Some logics allow a notion of infinitary disjunction. Indexed disjunction is existential quantification.

In dependent type theory

In dependent type theory, the disjunction of two mere propositions, PP and QQ, is the bracket type of their sum type, P+Q\| P + Q \|. Disjunction types in general could also be regarded as a particular sort of higher inductive type. In Coq syntax:

Inductive disjunction (P Q:Type) : Type :=
| inl : P -> disjunction P Q
| inr : Q -> disjunction P Q
| contr0 : forall (p q : disjunction P Q) p == q

If the dependent type theory has a type of propositions Prop\mathrm{Prop}, such as the one derived from a type universe UU - A:UisProp(A)\sum_{A:U} \mathrm{isProp}(A), then the disjunction of two types AA and BB is defined as the dependent function type

AB P:Prop((AP)×(BP))PA \vee B \equiv \prod_{P:\mathrm{Prop}} ((A \to P) \times (B \to P)) \to P

By weak function extensionality, the disjunction of two types is a proposition.

Theorem

The two definitions above are equivalent.

Proof

The propositional truncation of a type AA is equivalent to the following dependent function type

A P:Prop(AP)P\| A \| \simeq \prod_{P:\mathrm{Prop}} (A \to P) \to P

Substituting the sum type A+BA + B for AA, we have

A+B P:Prop((A+B)P)P\| A + B \| \simeq \prod_{P:\mathrm{Prop}} ((A + B) \to P) \to P

Given any type CC, there is an equivalence

((A+B)C)(AC)×(BC)((A + B) \to C) \simeq (A \to C) \times (B \to C)

and if ABA \simeq B, then (AC)(BC)(A \to C) \simeq (B \to C). In addition, for all type families x:AB(x)x:A \vdash B(x), and x:AC(x)x:A \vdash C(x), if there is a family of equivalences e: x:AB(x)C(x)e:\prod_{x:A} B(x) \simeq C(x), then there is an equivalence ( x:AB(x))( x:AC(x))\left(\prod_{x:A} B(x)\right) \simeq \left(\prod_{x:A} C(x)\right). All this taken together means that there are equivalences

A+B( P:Prop((A+B)P)P)( P:Prop((AP)×(BP))P)\| A + B \| \simeq \left(\prod_{P:\mathrm{Prop}} ((A + B) \to P) \to P\right) \simeq \left(\prod_{P:\mathrm{Prop}} ((A \to P) \times (B \to P)) \to P\right)

If one has the boolean domain and the existential quantifier, then the disjunction of two types AA and BB is given by the following type:

ABb:bool.((b=true)A)×((b=false)B)A \vee B \coloneqq \exists b:\mathrm{bool}.((b = \mathrm{true}) \to A) \times ((b = \mathrm{false}) \to B)

Classical vs constructive

There are a variety of connectives that are distinct in intuitionistic logic but are all equivalent to disjunction in classical logic. Here is a Hasse diagram of some of them, with the strongest statement at the bottom and the weakest at the top (so that each statement entails those above it):

¬(¬P¬Q) ¬PQ P¬Q (¬PQ)(P¬Q) PQ \array { & & \neg(\neg{P} \wedge \neg{Q}) \\ & ⇗ & & ⇖ \\ \neg{P} \rightarrow Q & & & & P \leftarrow \neg{Q} \\ & ⇖ & & ⇗ \\ & & (\neg{P} \rightarrow Q) \wedge (P \leftarrow \neg{Q}) \\ & & \Uparrow \\ & & P \vee Q }

(A single arrow is implication in the object language; a double arrow is entailment in the metalanguage.) Note that ¬P¬Q\neg{P} \wedge \neg{Q} is the negation of every item in this diagram.

In the double-negation interpretation? of classical logic in intuitionistic logic, ¬(¬P¬Q)\neg(\neg{P} \wedge \neg{Q}) is the interpretation in intuitionistic logic of disjunction in classical logic. For this reason, ¬(¬P¬Q)\neg(\neg{P} \wedge \neg{Q}) is sometimes called classical disjunction. But this doesn't mean that it should always be used when turning classical mathematics into constructive mathematics. Indeed, a stronger statement is almost always preferable, if one is valid; ¬(¬P¬Q)\neg(\neg{P} \wedge \neg{Q}) is merely the fallback position when nothing better can be found. (And as can be seen in the example in the paragraph after next, sometimes even this is not valid.)

In the antithesis interpretation of affine logic in intuitionistic logic, (¬PQ)(P¬Q)(\neg{P} \rightarrow Q) \wedge (P \leftarrow \neg{Q}) is the interpretation of the multiplicative disjunction PQP \parr Q for affirmative propositions. More generally, a statement PP in affine logic is interpreted as a pair (P +,P )(P^+,P^-) of mutually contradictory statements in intuitionistic logic; P P^- is simply the negation of P +P^+ for affirmative propositions, but in general, P P^- only entails ¬P +\neg{P^+}. Then PQP \parr Q is interpreted as ((P Q +)(P +Q ),P Q )\big((P^- \rightarrow Q^+) \wedge (P^+ \leftarrow Q^-), P^- \wedge Q^-\big); that is, (PQ) +(P \parr Q)^+ is (P Q +)(P +Q )(P^- \rightarrow Q^+) \wedge (P^+ \leftarrow Q^-), and (PQ) (P \parr Q)^- is P Q P^- \wedge Q^-. (In contrast, the additive disjunction PQP \oplus Q is interpreted as (P +Q +,P Q )(P^+ \vee Q^+, P^- \wedge Q^-). Note that PQP \oplus Q entails PQP \parr Q in affine logic, even though they are independent in linear logic.)

For a non-affirmative example, in the arithmetic of (located) real numbers, it is not constructively valid to derive (a=0)(b=0)(a = 0) \vee (b = 0) from ab=0a b = 0, and it's not even valid to derive ¬(¬(a=0)¬(b=0))\neg\big(\neg(a = 0) \wedge \neg(b = 0)\big) without Markov's principle (or at least some weak version of it), but it is valid to derive (a#0)(b=0)(a \# 0) \rightarrow (b = 0) (and conversely), where #\# is the usual apartness relation between real numbers. (Here, P +P^+ is a=0a = 0 and P P^- is a#0a \# 0, and similarly for QQ and bb.) Of course, it's also valid to derive ¬((a#0)(b#0))\neg\big((a \# 0) \wedge (b \# 0)\big) (which is actually equivalent).

Rules of inference

The rules of inference for disjunction in sequent calculus are dual to those for conjunction:

Γ,p,ΔΣ;Γ,q,ΔΣΓ,pq,ΔΣleft additive ΓΔ,p,ΣΓΔ,pq,Σright additive 0 ΓΔ,q,ΣΓΔ,pq,Σright additive 1 \begin {gathered} \frac { \Gamma , p , \Delta \vdash \Sigma ; \; \Gamma , q , \Delta \vdash \Sigma } { \Gamma , p \vee q , \Delta \vdash \Sigma } \; \text {left additive} \\ \frac { \Gamma \vdash \Delta , p , \Sigma } { \Gamma \vdash \Delta , p \vee q , \Sigma } \; \text {right additive 0} \\ \frac { \Gamma \vdash \Delta , q , \Sigma } { \Gamma \vdash \Delta , p \vee q , \Sigma } \; \text {right additive 1} \\ \end {gathered}

Equivalently, we can use the following rules with weakened contexts:

Γ,pΔ;q,ΣΠΓ,pq,ΣΔ,Πleft multiplicative ΓΔ,p,q,ΣΓΔ,pq,Σright multiplicative \begin {gathered} \frac { \Gamma , p \vdash \Delta ; \; q , \Sigma \vdash \Pi } { \Gamma , p \vee q , \Sigma \vdash \Delta , \Pi } \; \text {left multiplicative} \\ \frac { \Gamma \vdash \Delta , p , q , \Sigma } { \Gamma \vdash \Delta , p \vee q , \Sigma } \text {right multiplicative} \\ \end {gathered}

The rules above are written so as to remain valid in logics without the exchange rule. In linear logic, the first batch of sequent rules apply to additive disjunction (interpret pqp \vee q in these rules as pqp \oplus q), while the second batch of rules apply to multiplicative disjunction (interpret pqp \vee q in those rules as pqp \parr q).

The natural deduction rules for disjunction are a little more complicated than those for conjunction:

Γ,pr;Γ,qrΓ,pqrelimination ΓpΓpqintroduction 0 ΓqΓpqintroduction 1 \begin {gathered} \frac { \Gamma , p \vdash r ; \; \Gamma , q \vdash r } { \Gamma , p \vee q \vdash r } \; \text {elimination} \\ \frac { \Gamma \vdash p } { \Gamma \vdash p \vee q } \; \text {introduction 0} \\ \frac { \Gamma \vdash q } { \Gamma \vdash p \vee q } \; \text {introduction 1} \\ \end {gathered}
\phantom{-}symbol\phantom{-}\phantom{-}in logic\phantom{-}
A\phantom{A}\inA\phantom{A}element relation
A\phantom{A}:\,:A\phantom{A}typing relation
A\phantom{A}==A\phantom{A}equality
A\phantom{A}\vdashA\phantom{A}A\phantom{A}entailment / sequentA\phantom{A}
A\phantom{A}\topA\phantom{A}A\phantom{A}true / topA\phantom{A}
A\phantom{A}\botA\phantom{A}A\phantom{A}false / bottomA\phantom{A}
A\phantom{A}\RightarrowA\phantom{A}implication
A\phantom{A}\LeftrightarrowA\phantom{A}logical equivalence
A\phantom{A}¬\notA\phantom{A}negation
A\phantom{A}\neqA\phantom{A}negation of equality / apartnessA\phantom{A}
A\phantom{A}\notinA\phantom{A}negation of element relation A\phantom{A}
A\phantom{A}¬¬\not \notA\phantom{A}negation of negationA\phantom{A}
A\phantom{A}\existsA\phantom{A}existential quantificationA\phantom{A}
A\phantom{A}\forallA\phantom{A}universal quantificationA\phantom{A}
A\phantom{A}\wedgeA\phantom{A}logical conjunction
A\phantom{A}\veeA\phantom{A}logical disjunction
symbolin type theory (propositions as types)
A\phantom{A}\toA\phantom{A}function type (implication)
A\phantom{A}×\timesA\phantom{A}product type (conjunction)
A\phantom{A}++A\phantom{A}sum type (disjunction)
A\phantom{A}00A\phantom{A}empty type (false)
A\phantom{A}11A\phantom{A}unit type (true)
A\phantom{A}==A\phantom{A}identity type (equality)
A\phantom{A}\simeqA\phantom{A}equivalence of types (logical equivalence)
A\phantom{A}\sumA\phantom{A}dependent sum type (existential quantifier)
A\phantom{A}\prodA\phantom{A}dependent product type (universal quantifier)
symbolin linear logic
A\phantom{A}\multimapA\phantom{A}A\phantom{A}linear implicationA\phantom{A}
A\phantom{A}\otimesA\phantom{A}A\phantom{A}multiplicative conjunctionA\phantom{A}
A\phantom{A}\oplusA\phantom{A}A\phantom{A}additive disjunctionA\phantom{A}
A\phantom{A}&\&A\phantom{A}A\phantom{A}additive conjunctionA\phantom{A}
A\phantom{A}\invampA\phantom{A}A\phantom{A}multiplicative disjunctionA\phantom{A}
A\phantom{A}!\;!A\phantom{A}A\phantom{A}exponential conjunctionA\phantom{A}

References

  • Landon D. C. Elkind, Richard Zach, The Genealogy of \vee (arXiv:2012.06072)

The definition of the disjunction of two types in dependent type theory as the propositional truncation of the sum type is found in:

And the disjunction of two types defined from the type of propositions and dependent product types can be found in:

  • Madeleine Birchfield, Constructing coproduct types and boolean types from universes, MathOverflow (web)

Last revised on January 20, 2024 at 13:26:06. See the history of this page for a list of all contributions to it.