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 da Tabela 2.4.1 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 |
Tabela 2.4.1. As leis de negação dos quantificadores.
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! 🐙
2.4.1. Exemplos
Os exemplos abaixo aplicam as duas leis de negação e as combinam com os conectivos da Aula 1. Os Exemplos 6 e 10 raciocinam classicamente.
Exemplo 1. Uma propriedade que falha em toda parte não admite testemunha. Esta é a direção construtiva da primeira lei. O padrão de construtor anônimo em intro introduz o existencial e o destrói num só passo, então nenhum obtain é necessário.
example (α : Type) (P : α → Prop)
(h : ∀ x, ¬P x) : ¬∃ x, P x := α:TypeP:α → Proph:∀ (x : α), ¬P x⊢ ¬∃ x, P x
α:TypeP:α → Proph:∀ (x : α), ¬P xa:αhPa:P a⊢ False
All goals completed! 🐙
Exemplo 2. Reciprocamente, se não existe testemunha, a propriedade falha em cada elemento.
example (α : Type) (P : α → Prop)
(h : ¬∃ x, P x) : ∀ x, ¬P x := α:TypeP:α → Proph:¬∃ x, P x⊢ ∀ (x : α), ¬P x
α:TypeP:α → Proph:¬∃ x, P xa:αhPa:P a⊢ False
All goals completed! 🐙
Exemplo 3. Uma testemunha refuta a negação do existencial.
example (α : Type) (P : α → Prop)
(a : α) (hPa : P a) : ¬¬∃ x, P x := α:TypeP:α → Propa:αhPa:P a⊢ ¬¬∃ x, P x
α:TypeP:α → Propa:αhPa:P ahn:¬∃ x, P x⊢ False
All goals completed! 🐙
Exemplo 4. Uma propriedade que vale em toda parte exclui qualquer contraexemplo. A prova é um termo de prova, como na Aula 1. Como o objetivo negado é uma função em False, um fun que casa o padrão da testemunha do contraexemplo o prova.
example (α : Type) (P : α → Prop)
(h : ∀ x, P x) : ¬∃ x, ¬P x :=
fun ⟨a, hnPa⟩ => hnPa (h a)
Exemplo 5. Um contraexemplo refuta o enunciado universal. Esta é a direção construtiva da segunda lei.
example (α : Type) (P : α → Prop)
(h : ∃ x, ¬P x) : ¬∀ x, P x := α:TypeP:α → Proph:∃ x, ¬P x⊢ ¬∀ (x : α), P x
α:TypeP:α → Proph:∃ x, ¬P xhall:∀ (x : α), P x⊢ False
α:TypeP:α → Prophall:∀ (x : α), P xa:αhnPa:¬P a⊢ False
All goals completed! 🐙
Exemplo 6. A recíproca do Exemplo 4 exige raciocínio clássico. Dada a ausência de contraexemplos, Classical.byContradiction prova a propriedade em cada elemento.
example (α : Type) (P : α → Prop)
(h : ¬∃ x, ¬P x) : ∀ x, P x := α:TypeP:α → Proph:¬∃ x, ¬P x⊢ ∀ (x : α), P x
α:TypeP:α → Proph:¬∃ x, ¬P xa:α⊢ P a
α:TypeP:α → Proph:¬∃ x, ¬P xa:α⊢ ¬P a → False
α:TypeP:α → Proph:¬∃ x, ¬P xa:αhnPa:¬P a⊢ False
All goals completed! 🐙
Exemplo 7. Uma implicação ponto a ponto transporta a ausência de testemunhas da conclusão para a premissa. O padrão em intro de novo destrói o existencial na introdução.
example (α : Type) (P Q : α → Prop)
(h : ∀ x, P x → Q x) (hn : ¬∃ x, Q x) : ¬∃ x, P x := α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q xhn:¬∃ x, Q x⊢ ¬∃ x, P x
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q xhn:¬∃ x, Q xa:αhPa:P a⊢ False
All goals completed! 🐙
Exemplo 8. Quando nenhum elemento satisfaz as duas propriedades, cada elemento que satisfaz a primeira não satisfaz a segunda.
example (α : Type) (P Q : α → Prop)
(h : ¬∃ x, P x ∧ Q x) : ∀ x, P x → ¬Q x := α:TypeP:α → PropQ:α → Proph:¬∃ x, P x ∧ Q x⊢ ∀ (x : α), P x → ¬Q x
α:TypeP:α → PropQ:α → Proph:¬∃ x, P x ∧ Q xa:αhPa:P ahQa:Q a⊢ False
All goals completed! 🐙
Exemplo 9. A negação de um existencial de uma disjunção dá, em cada elemento, a conjunção das negações, o que combina a primeira lei com uma lei de De Morgan.
example (α : Type) (P Q : α → Prop)
(h : ¬∃ x, P x ∨ Q x) : ∀ x, ¬P x ∧ ¬Q x := α:TypeP:α → PropQ:α → Proph:¬∃ x, P x ∨ Q x⊢ ∀ (x : α), ¬P x ∧ ¬Q x
α:TypeP:α → PropQ:α → Proph:¬∃ x, P x ∨ Q xa:α⊢ ¬P a ∧ ¬Q a
α:TypeP:α → PropQ:α → Proph:¬∃ x, P x ∨ Q xa:α⊢ ¬P aα:TypeP:α → PropQ:α → Proph:¬∃ x, P x ∨ Q xa:α⊢ ¬Q a
α:TypeP:α → PropQ:α → Proph:¬∃ x, P x ∨ Q xa:α⊢ ¬P a α:TypeP:α → PropQ:α → Proph:¬∃ x, P x ∨ Q xa:αhPa:P a⊢ False
All goals completed! 🐙
α:TypeP:α → PropQ:α → Proph:¬∃ x, P x ∨ Q xa:α⊢ ¬Q a α:TypeP:α → PropQ:α → Proph:¬∃ x, P x ∨ Q xa:αhQa:Q a⊢ False
All goals completed! 🐙
Exemplo 10. O teorema not_forall_exists desta seção extrai um contraexemplo, e a implicação ponto a ponto o converte em testemunha.
example (α : Type) (P Q : α → Prop) (h : ¬∀ x, P x)
(hq : ∀ x, ¬P x → Q x) : ∃ x, Q x := α:TypeP:α → PropQ:α → Proph:¬∀ (x : α), P xhq:∀ (x : α), ¬P x → Q x⊢ ∃ x, Q x
α:TypeP:α → PropQ:α → Proph:¬∀ (x : α), P xhq:∀ (x : α), ¬P x → Q xa:αhnPa:¬P a⊢ ∃ x, Q x
All goals completed! 🐙