Conjunction

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Eléonore Mangel.

Created on 2022-02-08.
Last modified on 2024-04-11.

module foundation.conjunction where

open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.universal-property-cartesian-product-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.decidable-propositions
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.propositions

Idea

The conjunction^¶ P ∧ Q of two propositions P and Q is the proposition that both P and Q hold and is thus defined by the cartesian product of their underlying types

  P ∧ Q := P × Q

The conjunction of two propositions satisfies the universal property of the meet in the locale of propositions. This means that any span of propositions over P and Q factor (uniquely) through the conjunction

           R
        /  ∶  \
      /    ∶    \
    ∨      ∨      ∨
  P <--- P ∧ Q ---> Q.

In other words, we have a logical equivalence

  (R → P) ∧ (R → Q) ↔ (R → P ∧ Q)

for every proposition R. In fact, R can be any type.

The recursion principle^¶ of the conjunction of propositions states that to define a function P ∧ Q → R into a proposition R, or indeed any type, is equivalent to defining a function P → Q → R.

Definitions

The conjunction

module _
  {l1 l2 : Level} (P : Prop l1) (Q : Prop l2)
  where

  conjunction-Prop : Prop (l1 ⊔ l2)
  conjunction-Prop = product-Prop P Q

  type-conjunction-Prop : UU (l1 ⊔ l2)
  type-conjunction-Prop = type-Prop conjunction-Prop

  is-prop-conjunction-Prop :
    is-prop type-conjunction-Prop
  is-prop-conjunction-Prop = is-prop-type-Prop conjunction-Prop

  infixr  _∧_
  _∧_ : Prop (l1 ⊔ l2)
  _∧_ = conjunction-Prop

Note: The symbol used for the conjunction _∧_ is the logical and ∧ (agda-input: \wedge or \and).

The conjunction of decidable propositions

module _
  {l1 l2 : Level} (P : Decidable-Prop l1) (Q : Decidable-Prop l2)
  where

  is-decidable-conjunction-Decidable-Prop :
    is-decidable
      ( type-conjunction-Prop (prop-Decidable-Prop P) (prop-Decidable-Prop Q))
  is-decidable-conjunction-Decidable-Prop =
    is-decidable-product
      ( is-decidable-Decidable-Prop P)
      ( is-decidable-Decidable-Prop Q)

  conjunction-Decidable-Prop : Decidable-Prop (l1 ⊔ l2)
  conjunction-Decidable-Prop =
    ( type-conjunction-Prop (prop-Decidable-Prop P) (prop-Decidable-Prop Q) ,
      is-prop-conjunction-Prop (prop-Decidable-Prop P) (prop-Decidable-Prop Q) ,
      is-decidable-conjunction-Decidable-Prop)

The introduction rule and projections for the conjunction of propositions

While we define the introduction rule and projections for the conjunction below, we advice users to use the standard pairing and projection functions for the cartesian product types: pair, pr1 and pr2.

module _
  {l1 l2 : Level} (P : Prop l1) (Q : Prop l2)
  where

  intro-conjunction-Prop : type-Prop P → type-Prop Q → type-conjunction-Prop P Q
  intro-conjunction-Prop = pair

  pr1-conjunction-Prop : type-conjunction-Prop P Q → type-Prop P
  pr1-conjunction-Prop = pr1

  pr2-conjunction-Prop : type-conjunction-Prop P Q → type-Prop Q
  pr2-conjunction-Prop = pr2

The elimination principle of the conjunction

module _
  {l1 l2 : Level} (P : Prop l1) (Q : Prop l2)
  where

  ev-conjunction-Prop :
    {l : Level} (R : Prop l) → type-Prop (((P ∧ Q) ⇒ R) ⇒ P ⇒ Q ⇒ R)
  ev-conjunction-Prop R = ev-pair

  elimination-principle-conjunction-Prop : UUω
  elimination-principle-conjunction-Prop =
    {l : Level} (R : Prop l) → has-converse (ev-conjunction-Prop R)

Properties

The conjunction satisfies the recursion principle of the conjunction

module _
  {l1 l2 : Level} (P : Prop l1) (Q : Prop l2)
  where

  elim-conjunction-Prop : elimination-principle-conjunction-Prop P Q
  elim-conjunction-Prop R f (p , q) = f p q

The conjunction is the meet in the locale of propositions

module _
  {l1 l2 l3 : Level} (P : Prop l1) (Q : Prop l2) (C : UU l3)
  where

  map-distributive-conjunction-Prop :
    type-conjunction-Prop (function-Prop C P) (function-Prop C Q) →
    C → type-conjunction-Prop P Q
  map-distributive-conjunction-Prop (f , g) y = (f y , g y)

  map-inv-distributive-conjunction-Prop :
    (C → type-conjunction-Prop P Q) →
    type-conjunction-Prop (function-Prop C P) (function-Prop C Q)
  map-inv-distributive-conjunction-Prop f = (pr1 ∘ f , pr2 ∘ f)

  is-equiv-map-distributive-conjunction-Prop :
    is-equiv map-distributive-conjunction-Prop
  is-equiv-map-distributive-conjunction-Prop =
    is-equiv-has-converse
      ( conjunction-Prop (function-Prop C P) (function-Prop C Q))
      ( function-Prop C (conjunction-Prop P Q))
      ( map-inv-distributive-conjunction-Prop)

  distributive-conjunction-Prop :
    type-conjunction-Prop (function-Prop C P) (function-Prop C Q) ≃
    (C → type-conjunction-Prop P Q)
  distributive-conjunction-Prop =
    ( map-distributive-conjunction-Prop ,
      is-equiv-map-distributive-conjunction-Prop)

module _
  {l1 l2 l3 : Level} (P : Prop l1) (Q : Prop l2) (R : Prop l3)
  where

  is-greatest-binary-lower-bound-conjunction-Prop :
    type-Prop (((R ⇒ P) ∧ (R ⇒ Q)) ⇔ (R ⇒ P ∧ Q))
  is-greatest-binary-lower-bound-conjunction-Prop =
    ( map-distributive-conjunction-Prop P Q (type-Prop R) ,
      map-inv-distributive-conjunction-Prop P Q (type-Prop R))

See also

• The indexed counterpart to conjunction is universal quantification.

Table of files about propositional logic

The following table gives an overview of basic constructions in propositional logic and related considerations.

External links

• Logical conjunction at Mathswitch
• logical conjunction at $n$Lab
• Logical conjunction at Wikipedia

Recent changes

• 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
• 2024-02-06. Fredrik Bakke. Rename (co)prod to (co)product (#1017).
• 2023-12-12. Fredrik Bakke. Some minor refactoring surrounding Dedekind reals (#983).
• 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
• 2023-09-10. Fredrik Bakke. Define precedence levels and associativities for all binary operators (#712).