Why does Wolfram|Alpha not return True for following inputs:
trueQ[!(Exists[x,Exists[y,A[x,y]]] && !Exists[x,Exists[y,A[y,x]]])]
Simplify[!(Exists[x,Exists[y,A[x,y]]] && !Exists[x,Exists[y,A[y,x]]])]
?
The statement is obviously true, since first half before "and" claims that 2 things that satisfy A exist and second half after "and" claims that 2 such things do not exist(order of 2 existence quantifiers is not important), then this contradicting claim is negated. Is it a bug in Wolfram|Alpha, that it does not return true? Is trueQ or Simplify (or some other Wolfram function) supposed to (always) return true, if the argument is true (with every argument)? Would it even be possible to make an algorithm that understands if it's argument is true or not for every argument(with regard to Gödel 2. incompleteness theorem)? Which Wolfram's built-in function is best to determine if such logical statement with quantifiers are consistent or inconsistent?
