2.5. A Ordem dos Quantificadores🔗

Quantificadores consecutivos do mesmo tipo comutam, e quantificadores de tipos distintos não comutam. Uma direção da troca vale. 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.