nLab logical conjunction

Redirected from "additive conjunction".
Logical conjunction

Logical conjunction

Definitions

In logic, logical conjunction is the meet in the poset of truth values.

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

ppqqpqp \wedge q
TTTTTT
TTFFFF
FFTTFF
FFFFFF

That is, pqp \wedge q is true if and only if pp and qq are both true. Conjunction 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 conjunction 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 conjunction becomes intersection.

Remarks

Conjunction is de Morgan dual to disjunction.

Like any meet, conjunction is an associative operation, so we can take the conjunction of any finite positive whole number of truth values; the conjunction is true if and only if all of the individual truth values are true. Conjunction also has an identity element, which is the true truth value. Some logics allow a notion of infinitary conjunction. Indexed conjunction is universal quantification.

As truth values form a poset, which is a degenerate kind of category, so truth values under conjunction form a meet-semilattice, which is a degenerate kind of cartesian monoidal category. Self-referentially, a poset is (up to equivalence) simply a category enriched over the cartesian monoidal category of truth values. With implication as internal hom, truth values form a closed cartesian category.

In the context of substructural logics such as linear logic, the conjunction defined above is also called additive conjunction to disambiguate it from the multiplicative conjunction.

Rules of inference

That conjunction is a meet means that pqp \wedge q may be proved in a context Γ\Gamma if and only if both pp and qq may be proved in Γ\Gamma. This directly yields the introduction and elimination rules for conjunction in natural deduction:

Γp;ΓqΓpqintroduction ΓpqΓpelimination 0 ΓpqΓqelimination 1 \begin {gathered} \frac { \Gamma \vdash p ; \; \Gamma \vdash q } { \Gamma \vdash p \wedge q } \; \text {introduction} \\ \frac { \Gamma \vdash p \wedge q } { \Gamma \vdash p } \; \text {elimination 0} \\ \frac { \Gamma \vdash p \wedge q } { \Gamma \vdash q } \; \text {elimination 1} \\ \end {gathered}

Alternatively, we may use these slightly more complicated (but fewer) inductive forms:

Γp;ΓqΓpqintroduction Γ,p,qrΓ,pq,relimination \begin {gathered} \frac { \Gamma \vdash p ; \; \Gamma \vdash q } { \Gamma \vdash p \wedge q } \; \text {introduction} \\ \frac { \Gamma , p , q \vdash r } { \Gamma , p \wedge q , \vdash r } \; \text {elimination} \\ \end {gathered}

In sequent calculus, the same ideas become these rules:

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

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

ΓΔ,p;Σq,ΠΓ,ΣΔ,pq,Πright multiplicative Γ,p,q,ΔΣΓ,pq,ΔΣleft multiplicative \begin {gathered} \frac { \Gamma \vdash \Delta , p ; \; \Sigma \vdash q , \Pi } { \Gamma , \Sigma \vdash \Delta , p \wedge q , \Pi } \; \text {right multiplicative} \\ \frac { \Gamma , p , q , \Delta \vdash \Sigma } { \Gamma , p \wedge q , \Delta \vdash \Sigma } \text {left 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 conjunction (interpret pqp \wedge q in these rules as p&qp \& q), while the second batch of rules apply to multiplicative conjunction (interpret pqp \wedge q in those rules as pqp \otimes q).

As a logic gate

Logical conjunction as

  1. a logic gate,

  2. a reversible logic gate and

  3. a (reversible) quantum logic gate:

\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}
A\phantom{A}?\;?A\phantom{A}A\phantom{A}exponential disjunctionA\phantom{A}

Last revised on March 29, 2023 at 10:24:04. See the history of this page for a list of all contributions to it.