I have a habit of trying out correctness about some logical statements with worlfram alpha by generating truth table for them. For example, I can try if this:
$$((¬x→y)∧(¬x→¬y))→x$$
is correct or not by generating truth table for $((¬x→y)∧(¬x→¬y))$ which turns out to be the same as $x$ column in the same truth table. Hence the above is correct. However is there any way I can check same for biconditionals involving nested existential and universal quantifiers and predicates? For example can I somehow verify rules of this kind?:
$$(∀x)(∀y)ϕ(x,y)⇔(∀y)(∀x)ϕ(x,y)$$
Update
I am able to do following check $∀x,y(x∨y)$ as follows:
Resolve[ForAll[{x,y}, x or y]]
which correctly returns $False$ as $(x∨y)$ does not hold for all $x$ and $y$.
So now I thought I can do something similar to obtain $True$ for following (which is a general fact): $¬(∀x)ϕ(x)⇔(∃x)¬ϕ(x)$. I tried this:
Resolve[ForAll[x,(not ForAll[x, x]) xnor (exists[x,not x])]]
But it did not work. Note that $⇔$ is nothing but XNOR. So how do I do this especially something like following also correctly returns $True$:
which stands for $¬∀x(x)$.