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)
.