Czy powyższa formuła jest tautologią? Klaudia: ∃x∀y : ϕ(x, y) ⇒[¬∀x : ϕ(x, x) ∨ ∃x : ϕ(x, x)];

Gray: Tak. Jeżeli prawdą jest, że ∃x∀y : Φ(x,y), to w szczególności dla y=x zachodzi Φ(x,x). To oznacza, że warunek "∃x : ϕ(x, x)" jest prawdziwy, zatem cała alternatywa "¬∀x : ϕ(x, x) ∨ ∃x : ϕ(x, x)" również. Jeżeli zaś warunek ∃x∀y : Φ(x,y) nie zachodzi, to cała implikacja jest również prawdziwa (z oczywistych względów).