Message Boards Message Boards

Using W|A to check biconditional involving predicates?

GROUPS:

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 geerating truth table for [((¬x→y)∧(¬x→¬y))](http://www.wolframalpha.com/input/?i=((not+x+implies+y)+and+(not+x+implies+not+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])]]](http://www.wolframalpha.com/input/?i=Resolve%5BForAll%5Bx,(not+ForAll%5Bx,+x%5D)+xnor+(exists%5Bx,not+x%5D)%5D%5D)

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:

Resolve[not ForAll[x, x]]

which stands for ¬∀x(x).

POSTED BY: Mahesh Abnave
Answer
11 months ago

Group Abstract Group Abstract