Existential quantification
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.
Created on 2022-02-08.
Last modified on 2024-09-23.
module foundation.existential-quantification where
Imports
open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.functoriality-propositional-truncation open import foundation.logical-equivalences open import foundation.propositional-extensionality open import foundation.propositional-truncations open import foundation.universe-levels open import foundation-core.cartesian-product-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types open import foundation-core.propositions
Idea
Given a family of propositions P
over A
,
the
existential quantification¶
of P
over A
is the proposition ∃ A P
asserting that there is an element
a : A
such that P a
holds. We use the
propositional truncation to define
the existential quantification,
∃ (x : A), (P x) := ║ Σ (x : A), (P x) ║₋₁
because the
Curry–Howard interpretation
of the existential quantification as Σ A P
does not guarantee that existential
quantifications are interpreted as propositions.
The
universal property¶
of existential quantification states that it is the
least upper 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
(∀ (x : A), (P x ⇒ Q)) ⇔ ((∃ (x : A), (P x)) ⇒ Q).
Definitions
Existence of structure
Given a structure B : A → 𝒰
on a type A
, the
propositional truncation
║ Σ (x : A), (B x) ║₋₁
satisfies the universal property of the existential quantification
∃ (x : A), ║ B x ║₋₁
and is thus equivalent to it. Therefore, we may reasonably call this
construction the
existential quantification¶
of structure. It is important to keep in mind that this is not a generalization
of the concept but rather a conflation, and should be read as the statement the
type of elements x : A
equipped with y : B x
is
inhabited.
Existence of structure is a widely occurring notion in univalent mathematics.
For instance, the condition that an element y : B
is in the
image of a map f : A → B
is formulated using existence
of structure: The element y
is in the image of f
if the type of x : A
equipped with an identification f x = y
is inhabited.
Because subtypes are a special case of structure, and Agda can generally infer
structures for us, we will continue to conflate the two in our formalizations
for the benefit that we have to specify the subtype in our code less often. For
instance, even though the introduction rule for existential quantification
intro-exists
is phrased in terms of existential quantification on structures,
it equally applies to existential quantification on subtypes.
module _ {l1 l2 : Level} (A : UU l1) (B : A → UU l2) where exists-structure-Prop : Prop (l1 ⊔ l2) exists-structure-Prop = trunc-Prop (Σ A B) exists-structure : UU (l1 ⊔ l2) exists-structure = type-Prop exists-structure-Prop is-prop-exists-structure : is-prop exists-structure is-prop-exists-structure = is-prop-type-Prop exists-structure-Prop
Existential quantification
module _ {l1 l2 : Level} (A : UU l1) (P : A → Prop l2) where exists-Prop : Prop (l1 ⊔ l2) exists-Prop = exists-structure-Prop A (type-Prop ∘ P) exists : UU (l1 ⊔ l2) exists = type-Prop exists-Prop abstract is-prop-exists : is-prop exists is-prop-exists = is-prop-type-Prop exists-Prop ∃ : Prop (l1 ⊔ l2) ∃ = exists-Prop
The introduction rule for existential quantification
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where intro-exists : (a : A) (b : B a) → exists-structure A B intro-exists a b = unit-trunc-Prop (a , b)
Note. Even though the introduction rule is formalized in terms of existential quantification on structures, it equally applies to existential quantification on subtypes. This is because subtypes are a special case of structure. The benefit of this approach is that Agda can infer structures for us, but not generally subtypes.
The universal property of existential quantification
module _ {l1 l2 l3 : Level} (A : UU l1) (B : A → UU l2) (S : Prop l3) where universal-property-exists-structure : UUω universal-property-exists-structure = {l : Level} (Q : Prop l) → (type-Prop S → type-Prop Q) ↔ ((x : A) → B x → type-Prop Q) module _ {l1 l2 l3 : Level} (A : UU l1) (P : A → Prop l2) (S : Prop l3) where universal-property-exists : UUω universal-property-exists = universal-property-exists-structure A (type-Prop ∘ P) S
Properties
The elimination rule of existential quantification
The
universal property¶
of existential quantification states ∃ A P
is the least upper bound on the
predicate P
in the locale of propositions.
module _ {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} where ev-intro-exists : {C : UU l3} → (exists-structure A B → C) → (x : A) → B x → C ev-intro-exists H x p = H (intro-exists x p) elim-exists : (Q : Prop l3) → ((x : A) → B x → type-Prop Q) → (exists-structure A B → type-Prop Q) elim-exists Q f = map-universal-property-trunc-Prop Q (ind-Σ f) abstract is-equiv-ev-intro-exists : (Q : Prop l3) → is-equiv (ev-intro-exists {type-Prop Q}) is-equiv-ev-intro-exists Q = is-equiv-has-converse ( function-Prop (exists-structure A B) Q) ( Π-Prop A (λ x → function-Prop (B x) Q)) ( elim-exists Q)
The existential quantification satisfies the universal property of existential quantification
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where up-exists : universal-property-exists-structure A B (exists-structure-Prop A B) up-exists Q = (ev-intro-exists , elim-exists Q)
Propositions that satisfy the universal property of a existential quantification are equivalent to the existential quantification
module _ {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (Q : Prop l3) (up-Q : universal-property-exists-structure A B Q) where forward-implication-iff-universal-property-exists : exists-structure A B → type-Prop Q forward-implication-iff-universal-property-exists = elim-exists Q (forward-implication (up-Q Q) id) backward-implication-iff-universal-property-exists : type-Prop Q → exists-structure A B backward-implication-iff-universal-property-exists = backward-implication (up-Q (exists-structure-Prop A B)) intro-exists iff-universal-property-exists : exists-structure A B ↔ type-Prop Q iff-universal-property-exists = ( forward-implication-iff-universal-property-exists , backward-implication-iff-universal-property-exists)
Existential quantification of structure is the same as existential quantification over its propositional reflection
We proceed by showing that the latter satisfies the universal property of the former.
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where universal-property-exists-structure-exists-trunc-Prop : universal-property-exists-structure A B (exists-Prop A (trunc-Prop ∘ B)) universal-property-exists-structure-exists-trunc-Prop Q = ( λ f a b → f (unit-trunc-Prop (a , unit-trunc-Prop b))) , ( λ f → rec-trunc-Prop Q (λ (a , |b|) → rec-trunc-Prop Q (f a) |b|)) compute-exists-trunc-Prop : exists-structure A B ↔ exists A (trunc-Prop ∘ B) compute-exists-trunc-Prop = iff-universal-property-exists ( exists-Prop A (trunc-Prop ∘ B)) ( universal-property-exists-structure-exists-trunc-Prop)
Taking the cartesian product with a proposition distributes over existential quantification of structures
module _ {l1 l2 l3 : Level} (P : Prop l1) {A : UU l2} {B : A → UU l3} where map-distributive-product-exists-structure : type-Prop P × exists-structure A B → exists-structure A (λ x → type-Prop P × B x) map-distributive-product-exists-structure (p , e) = elim-exists ( exists-structure-Prop A (λ x → type-Prop P × B x)) ( λ x q → intro-exists x (p , q)) ( e) map-inv-distributive-product-exists-structure : exists-structure A (λ x → type-Prop P × B x) → type-Prop P × exists-structure A B map-inv-distributive-product-exists-structure = elim-exists ( P ∧ exists-structure-Prop A B) ( λ x (p , q) → (p , intro-exists x q)) iff-distributive-product-exists-structure : ( type-Prop P × exists-structure A B) ↔ ( exists-structure A (λ x → type-Prop P × B x)) iff-distributive-product-exists-structure = ( map-distributive-product-exists-structure , map-inv-distributive-product-exists-structure) eq-distributive-product-exists-structure : P ∧ exists-structure-Prop A B = exists-structure-Prop A (λ x → type-Prop P × B x) eq-distributive-product-exists-structure = eq-iff' ( P ∧ exists-structure-Prop A B) ( exists-structure-Prop A (λ x → type-Prop P × B x)) ( iff-distributive-product-exists-structure)
Conjunction distributes over existential quantification
module _ {l1 l2 l3 : Level} (P : Prop l1) {A : UU l2} (Q : A → Prop l3) where map-distributive-conjunction-exists : type-Prop (P ∧ (∃ A Q) ⇒ ∃ A (λ x → P ∧ Q x)) map-distributive-conjunction-exists = map-distributive-product-exists-structure P map-inv-distributive-conjunction-exists : type-Prop (∃ A (λ x → P ∧ Q x) ⇒ P ∧ (∃ A Q)) map-inv-distributive-conjunction-exists = map-inv-distributive-product-exists-structure P iff-distributive-conjunction-exists : type-Prop (P ∧ ∃ A Q ⇔ ∃ A (λ x → P ∧ Q x)) iff-distributive-conjunction-exists = iff-distributive-product-exists-structure P eq-distributive-conjunction-exists : P ∧ (∃ A Q) = ∃ A (λ x → P ∧ Q x) eq-distributive-conjunction-exists = eq-distributive-product-exists-structure P
See also
- Existential quantification is the indexed counterpart to disjunction
Table of files about propositional logic
The following table gives an overview of basic constructions in propositional logic and related considerations.
External links
- Existential quantification at Mathswitch
- existential quantifier at Lab
Recent changes
- 2024-09-23. Fredrik Bakke. Cantor's theorem and diagonal argument (#1185).
- 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
- 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-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644).