2.4. Leis de Negação dos Quantificadores
As leis de De Morgan da Aula 1 trocam a negação com a conjunção e a disjunção. As leis abaixo trocam a negação com os quantificadores.
Nome | Equivalência |
|---|---|
Negação de ∃ | ¬(∃ x, P x) ≡ ∀ x, ¬P x |
Negação de ∀ | ¬(∀ x, P x) ≡ ∃ x, ¬P x |
A primeira lei é construtiva nas duas direções.
theorem not_exists_iff (α : Type) (P : α → Prop) :
¬(∃ x, P x) ↔ ∀ x, ¬P x := α:TypeP:α → Prop⊢ (¬∃ x, P x) ↔ ∀ (x : α), ¬P x
α:TypeP:α → Prop⊢ (¬∃ x, P x) → ∀ (x : α), ¬P xα:TypeP:α → Prop⊢ (∀ (x : α), ¬P x) → ¬∃ x, P x
α:TypeP:α → Prop⊢ (¬∃ x, P x) → ∀ (x : α), ¬P x α:TypeP:α → Proph:¬∃ x, P xa:αhPa:P a⊢ False
All goals completed! 🐙
α:TypeP:α → Prop⊢ (∀ (x : α), ¬P x) → ¬∃ x, P x α:TypeP:α → Proph:∀ (x : α), ¬P xhex:∃ x, P x⊢ False
α:TypeP:α → Proph:∀ (x : α), ¬P xa:αhPa:P a⊢ False
All goals completed! 🐙
Na segunda lei, a direção de ∃ x, ¬P x para ¬(∀ x, P x) é construtiva, e a direção recíproca requer raciocínio clássico, como a primeira lei de De Morgan na Aula 1. Duas aplicações de Classical.byContradiction produzem a testemunha.
theorem not_forall_exists (α : Type) (P : α → Prop)
(h : ¬∀ x, P x) : ∃ x, ¬P x := α:TypeP:α → Proph:¬∀ (x : α), P x⊢ ∃ x, ¬P x
α:TypeP:α → Proph:¬∀ (x : α), P x⊢ (¬∃ x, ¬P x) → False
α:TypeP:α → Proph:¬∀ (x : α), P xhne:¬∃ x, ¬P x⊢ False
α:TypeP:α → Proph:¬∀ (x : α), P xhne:¬∃ x, ¬P x⊢ ∀ (x : α), P x
α:TypeP:α → Proph:¬∀ (x : α), P xhne:¬∃ x, ¬P xa:α⊢ P a
α:TypeP:α → Proph:¬∀ (x : α), P xhne:¬∃ x, ¬P xa:α⊢ ¬P a → False
α:TypeP:α → Proph:¬∀ (x : α), P xhne:¬∃ x, ¬P xa:αhnPa:¬P a⊢ False
All goals completed! 🐙