Universal quantification

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-04-11.
Last modified on 2024-04-11.

module foundation.universal-quantification where

open import foundation.dependent-pair-types
open import foundation.evaluation-functions
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.propositions

Idea

Given a type A and a subtype P : A → Prop, the universal quantification^¶

  ∀ (x : A), (P x)

is the proposition that there exists a proof of P x for every x in A.

The universal property^¶ of universal quantification states that it is the greatest lower bound on the family of propositions P in the locale of propositions, by which we mean that for every proposition Q we have the logical equivalence

  (∀ (a : A), (R → P a)) ↔ (R → ∀ (a : A), (P a))

Notation. Because of syntactic limitations of the Agda language, we cannot use ∀ for the universal quantification in formalizations, and instead use ∀'.

Definitions

Universal quantification

module _
  {l1 l2 : Level} (A : UU l1) (P : A → Prop l2)
  where

  for-all-Prop : Prop (l1 ⊔ l2)
  for-all-Prop = Π-Prop A P

  type-for-all-Prop : UU (l1 ⊔ l2)
  type-for-all-Prop = type-Prop for-all-Prop

  is-prop-for-all-Prop : is-prop type-for-all-Prop
  is-prop-for-all-Prop = is-prop-type-Prop for-all-Prop

  for-all : UU (l1 ⊔ l2)
  for-all = type-for-all-Prop

  ∀' : Prop (l1 ⊔ l2)
  ∀' = for-all-Prop

The universal property of universal quantification

The universal property^¶ of the universal quantification ∀ (a : A), (P a) states that for every proposition R, the canonical map

  (∀ (a : A), (R → P a)) → (R → ∀ (a : A), (P a))

is a logical equivalence. Indeed, this holds for any type R.

module _
  {l1 l2 : Level} (A : UU l1) (P : A → Prop l2)
  where

  universal-property-for-all : {l3 : Level} (S : Prop l3) → UUω
  universal-property-for-all S =
    {l : Level} (R : Prop l) →
    type-Prop ((∀' A (λ a → R ⇒ P a)) ⇔ (R ⇒ S))

  ev-for-all :
    {l : Level} {B : UU l} →
    for-all A (λ a → function-Prop B (P a)) → B → for-all A P
  ev-for-all f r a = f a r

Properties

Universal quantification satisfies its universal property

module _
  {l1 l2 : Level} (A : UU l1) (P : A → Prop l2)
  where

  map-up-for-all :
    {l : Level} {B : UU l} →
    (B → for-all A P) → for-all A (λ a → function-Prop B (P a))
  map-up-for-all f a r = f r a

  is-equiv-ev-for-all :
    {l : Level} {B : UU l} → is-equiv (ev-for-all A P {B = B})
  is-equiv-ev-for-all {B = B} =
    is-equiv-has-converse
      ( ∀' A (λ a → function-Prop B (P a)))
      ( function-Prop B (∀' A P))
      ( map-up-for-all)

  up-for-all : universal-property-for-all A P (∀' A P)
  up-for-all R = (ev-for-all A P , map-up-for-all)

See also

• Universal quantification is the indexed counterpart to conjunction.

Table of files about propositional logic

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

External links

• Universal quantification at Mathswitch
• universal quantifier at $n$Lab
• Universal quantification at Wikipedia

Recent changes

• 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).