2.5. A Ordem dos Quantificadores🔗

A ordem dos quantificadores determina o que um enunciado afirma. Em ∀ y, ∃ x, R x y, a testemunha x pode depender de y, e valores distintos de y podem exigir testemunhas distintas. Em ∃ x, ∀ y, R x y, uma única testemunha x satisfaz R com todo y de uma vez. A segunda forma afirma uma testemunha uniforme, então é o enunciado mais forte.

Quantificadores do mesmo tipo comutam, e os exemplos das duas seções anteriores provaram as trocas para ∀ e para ∃. Quantificadores de tipos distintos não comutam, e apenas uma direção da troca vale. A ordem mais forte implica a mais fraca. Uma testemunha que satisfaz R com todo y em particular satisfaz R com cada y dado.

theorem exists_forall_swap (α β : Type) (R : α → β → Prop)
    (h : ∃ x, ∀ y, R x y) : ∀ y, ∃ x, R x y := byα:Typeβ:TypeR:α → β → Proph:∃ x, ∀ (y : β), R x y⊢ ∀ (y : β), ∃ x, R x y
  intro bα:Typeβ:TypeR:α → β → Proph:∃ x, ∀ (y : β), R x yb:β⊢ ∃ x, R x b
  obtain ⟨a, ha⟩ := hα:Typeβ:TypeR:α → β → Propb:βa:αha:∀ (y : β), R a y⊢ ∃ x, R x b
  exact ⟨a, ha b⟩All goals completed! 🐙

A recíproca falha. Sobre os números naturais, tome R x y como x ≥ y. Então ∀ y, ∃ x, R x y vale, pois cada y satisfaz y ≥ y, e ∃ x, ∀ y, R x y afirma que algum número natural é maior ou igual a todo número natural, o que é falso.

2.5.1. Exemplos🔗

Os exemplos abaixo movem quantificadores uns sobre os outros. Os dois últimos provam em Lean as duas afirmações do contraexemplo acima.

Exemplo 1. Uma testemunha que se relaciona com todo elemento em particular se relaciona consigo mesma.

example (α : Type) (R : α → α → Prop)
    (h : ∃ x, ∀ y, R x y) : ∃ x, R x x := byα:TypeR:α → α → Proph:∃ x, ∀ (y : α), R x y⊢ ∃ x, R x x
  obtain ⟨a, ha⟩ := hα:TypeR:α → α → Propa:αha:∀ (y : α), R a y⊢ ∃ x, R x x
  exact ⟨a, ha a⟩All goals completed! 🐙

Exemplo 2. Um enunciado existencial-universal dá o duplamente existencial quando o tipo interno tem um elemento.

example (α β : Type) (R : α → β → Prop) (b : β)
    (h : ∃ x, ∀ y, R x y) : ∃ x, ∃ y, R x y := byα:Typeβ:TypeR:α → β → Propb:βh:∃ x, ∀ (y : β), R x y⊢ ∃ x y, R x y
  obtain ⟨a, ha⟩ := hα:Typeβ:TypeR:α → β → Propb:βa:αha:∀ (y : β), R a y⊢ ∃ x y, R x y
  exact ⟨a, b, ha b⟩All goals completed! 🐙

Exemplo 3. Um enunciado duplamente universal dá a ordem mista quando o tipo das testemunhas tem um elemento.

example (α β : Type) (R : α → β → Prop) (a : α)
    (h : ∀ x, ∀ y, R x y) : ∀ y, ∃ x, R x y := byα:Typeβ:TypeR:α → β → Propa:αh:∀ (x : α) (y : β), R x y⊢ ∀ (y : β), ∃ x, R x y
  intro bα:Typeβ:TypeR:α → β → Propa:αh:∀ (x : α) (y : β), R x yb:β⊢ ∃ x, R x b
  exact ⟨a, h a b⟩All goals completed! 🐙

Exemplo 4. O teorema exists_forall_swap é uma função, e aplicá-lo a uma hipótese e a um elemento dá a conclusão instanciada. A prova é a própria aplicação.

example (α β : Type) (R : α → β → Prop)
    (h : ∃ x, ∀ y, R x y) (b : β) : ∃ x, R x b :=
  exists_forall_swap α β R h b

Exemplo 5. Uma conjunção sob os dois quantificadores projeta-se na sua parte esquerda, preservando a testemunha.

example (α β : Type) (R S : α → β → Prop)
    (h : ∃ x, ∀ y, R x y ∧ S x y) : ∃ x, ∀ y, R x y := byα:Typeβ:TypeR:α → β → PropS:α → β → Proph:∃ x, ∀ (y : β), R x y ∧ S x y⊢ ∃ x, ∀ (y : β), R x y
  obtain ⟨a, ha⟩ := hα:Typeβ:TypeR:α → β → PropS:α → β → Propa:αha:∀ (y : β), R a y ∧ S a y⊢ ∃ x, ∀ (y : β), R x y
  exists aα:Typeβ:TypeR:α → β → PropS:α → β → Propa:αha:∀ (y : β), R a y ∧ S a y⊢ ∀ (y : β), R a y
  intro bα:Typeβ:TypeR:α → β → PropS:α → β → Propa:αha:∀ (y : β), R a y ∧ S a yb:β⊢ R a b
  exact (ha b).leftAll goals completed! 🐙

Exemplo 6. Duas hipóteses existencial-universais combinam-se numa conjunção duplamente existencial, e cada testemunha instancia o universal da outra.

example (α β : Type) (R S : α → β → Prop)
    (h1 : ∃ x, ∀ y, R x y) (h2 : ∃ y, ∀ x, S x y) :
    ∃ x, ∃ y, R x y ∧ S x y := byα:Typeβ:TypeR:α → β → PropS:α → β → Proph1:∃ x, ∀ (y : β), R x yh2:∃ y, ∀ (x : α), S x y⊢ ∃ x y, R x y ∧ S x y
  obtain ⟨a, ha⟩ := h1α:Typeβ:TypeR:α → β → PropS:α → β → Proph2:∃ y, ∀ (x : α), S x ya:αha:∀ (y : β), R a y⊢ ∃ x y, R x y ∧ S x y
  obtain ⟨b, hb⟩ := h2α:Typeβ:TypeR:α → β → PropS:α → β → Propa:αha:∀ (y : β), R a yb:βhb:∀ (x : α), S x b⊢ ∃ x y, R x y ∧ S x y
  exact ⟨a, b, ha b, hb a⟩All goals completed! 🐙

Exemplo 7. Com três quantificadores, a testemunha existencial serve para todo z, então o universal externo move-se para a frente.

example (α β γ : Type) (T : α → β → γ → Prop)
    (h : ∃ x, ∀ y, ∀ z, T x y z) :
    ∀ z, ∃ x, ∀ y, T x y z := byα:Typeβ:Typeγ:TypeT:α → β → γ → Proph:∃ x, ∀ (y : β) (z : γ), T x y z⊢ ∀ (z : γ), ∃ x, ∀ (y : β), T x y z
  intro cα:Typeβ:Typeγ:TypeT:α → β → γ → Proph:∃ x, ∀ (y : β) (z : γ), T x y zc:γ⊢ ∃ x, ∀ (y : β), T x y c
  obtain ⟨a, ha⟩ := hα:Typeβ:Typeγ:TypeT:α → β → γ → Propc:γa:αha:∀ (y : β) (z : γ), T a y z⊢ ∃ x, ∀ (y : β), T x y c
  exists aα:Typeβ:Typeγ:TypeT:α → β → γ → Propc:γa:αha:∀ (y : β) (z : γ), T a y z⊢ ∀ (y : β), T a y c
  intro bα:Typeβ:Typeγ:TypeT:α → β → γ → Propc:γa:αha:∀ (y : β) (z : γ), T a y zb:β⊢ T a b c
  exact ha b cAll goals completed! 🐙

Exemplo 8. A contraposição de exists_forall_swap transporta a negação na direção oposta.

example (α β : Type) (R : α → β → Prop)
    (h : ¬∀ y, ∃ x, R x y) : ¬∃ x, ∀ y, R x y := byα:Typeβ:TypeR:α → β → Proph:¬∀ (y : β), ∃ x, R x y⊢ ¬∃ x, ∀ (y : β), R x y
  intro hexα:Typeβ:TypeR:α → β → Proph:¬∀ (y : β), ∃ x, R x yhex:∃ x, ∀ (y : β), R x y⊢ False
  exact h (exists_forall_swap α β R hex)All goals completed! 🐙

Exemplo 9. A primeira afirmação do contraexemplo acima. Cada número natural é maior ou igual a si mesmo.

example : ∀ y : Nat, ∃ x : Nat, x ≥ y := by⊢ ∀ (y : Nat), ∃ x, x ≥ y
  intro bb:Nat⊢ ∃ x, x ≥ b
  exact ⟨b, Nat.le_refl b⟩All goals completed! 🐙

Exemplo 10. A segunda afirmação. Nenhum número natural é maior ou igual a todo número natural, pois a + 1 excede a. O lema Nat.not_succ_le_self refuta a ≥ a + 1.

example : ¬∃ x : Nat, ∀ y : Nat, x ≥ y := by⊢ ¬∃ x, ∀ (y : Nat), x ≥ y
  intro ⟨a, ha⟩a:Natha:∀ (y : Nat), a ≥ y⊢ False
  exact absurd (ha (a + 1)) (Nat.not_succ_le_self a)All goals completed! 🐙