De Morgan’s law for finite families of propositions

Content created by Fredrik Bakke.

Created on 2025-01-07.
Last modified on 2025-01-07.

module univalent-combinatorics.de-morgans-law where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.coproduct-types
open import foundation.decidable-dependent-pair-types
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equivalences
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.negation
open import foundation.unit-type
open import foundation.universe-levels

open import logic.de-morgan-propositions
open import logic.de-morgan-types

open import univalent-combinatorics.counting
open import univalent-combinatorics.standard-finite-types

Idea

Given a finite family of De Morgan types P : Fin k → De-Morgan-Type, then the finitary De Morgan’s law

  ¬ (∀ i, P i) ⇒ ∃ i, ¬ (P i)

holds.

Result

cases-decide-de-morgans-law-family-Fin-is-de-morgan-family :
  {l : Level} (k : ℕ) {P : Fin (succ-ℕ k) → UU l} →
  ((x : Fin (succ-ℕ k)) → is-de-morgan (P x)) →
  ¬ ((x : Fin (succ-ℕ k)) → P x) →
  ¬ P (inr star) + ¬ ((x : Fin k) → P (inl x))
cases-decide-de-morgans-law-family-Fin-is-de-morgan-family k {P} H q =
  rec-coproduct
    ( inl)
    ( λ z → inr (λ y → z (λ y' → q (ind-coproduct P y (λ _ → y')))))
    ( H (inr star))

decide-de-morgans-law-family-Fin-is-de-morgan-family :
  {l : Level} (k : ℕ) {P : Fin k → UU l} →
  ((x : Fin k) → is-de-morgan (P x)) →
  ¬ ((x : Fin k) → P x) →
  Σ (Fin k) (¬_ ∘ P)
decide-de-morgans-law-family-Fin-is-de-morgan-family zero-ℕ {P} H q =
  q (λ ()) , (λ x → q (λ ()))
decide-de-morgans-law-family-Fin-is-de-morgan-family (succ-ℕ k) {P} H q =
  rec-coproduct
    ( inr star ,_)
    ( λ q' →
      map-Σ-map-base inl
        ( ¬_ ∘ P)
        ( decide-de-morgans-law-family-Fin-is-de-morgan-family k (H ∘ inl) q'))
    ( cases-decide-de-morgans-law-family-Fin-is-de-morgan-family k H q)

module _
  {l : Level} {k : ℕ} (P : Fin k → De-Morgan-Type l)
  where

  decide-de-morgans-law-family-family-Fin :
    ¬ ((x : Fin k) → type-De-Morgan-Type (P x)) →
    Σ (Fin k) (¬_ ∘ type-De-Morgan-Type ∘ P)
  decide-de-morgans-law-family-family-Fin =
    decide-de-morgans-law-family-Fin-is-de-morgan-family k
      ( is-de-morgan-type-De-Morgan-Type ∘ P)

Comment

It is likely that this finitary De Morgan’s law can be generalized to families of De Morgan types indexed by searchable types in the sense of Escardó [Esc08].

References

[Esc08]
Martín Hötzel Escardó. Exhaustible sets in higher-type computation. Logical Methods in Computer Science, 4(3):3:3, 37, 8 2008. arXiv:0808.0441, doi:10.2168/LMCS-4(3:3)2008.

Recent changes