Message Boards Message Boards

0
|
4041 Views
|
6 Replies
|
0 Total Likes
View groups...
Share
Share this post:

Is there a function, that simplifies logical statements?

Olger Männik
Posted 2 years ago

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?
POSTED BY: Olger Männik
6 Replies
Sort By:

Simplify can simplify some logical expression, for example

Simplify[a && b && a]
Simplify[And[Or[a, c], Or[a, d]]]
POSTED BY: Gianluca Gorni

Here is a simpler example:

FullSimplify[Equivalent[Exists[x, A[x]], Exists[y, A[y]]]]

My guess is that either logical simplification does not handle expression as generic as A[x], or that replacing a dummy variable with another is not among the rules tried in the simplification.

This may be vaguely similar:

Simplify[f'[x]^2 >= 0, Element[f[x], Reals]]
POSTED BY: Gianluca Gorni
Bill Nelson
Bill Nelson
Posted 2 years ago 
!(Exists[x,Exists[y,A[x,y]]] && !Exists[x,Exists[y,A[x,y]]])

returns True

as does

TrueQ[!(Exists[x,Exists[y,A[x,y]]] && !Exists[x,Exists[y,A[x,y]]])]

as does

Simplify[!(Exists[x,Exists[y,A[x,y]]] && !Exists[x,Exists[y,A[x,y]]])]

! link

TrueQ link

Simplify link
POSTED BY: Bill Nelson
Olger Männik
Olger Männik
Posted 2 years ago

Is there any function in Wolfram, that is able to understand, that !(Exists[x,Exists[y,A[x,y]]] && !Exists[x,Exists[y,A[y,x]]]) is true?
POSTED BY: Olger Männik
Rohit Namjoshi
Rohit Namjoshi
Posted 2 years ago

Maybe try FindEquationalProof.
POSTED BY: Rohit Namjoshi

These examples are along the same lines:

FullSimplify[
 Integrate[f[x], {x, 0, 1}] == Integrate[f[y], {y, 0, 1}]]
FullSimplify[Sum[f[n], {n, a, b}] == Sum[f[m], {m, a, b}]]

My guess is that a replacement of dummy variables is not among the transformations used by Simplify.
POSTED BY: Gianluca Gorni
Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Tag limit exceeded
Note: Only the first five people you tag will receive an email notification; the other tagged names will appear as links to their profiles.
Reply Preview
Attachments
Remove
or Discard

Group Abstract Group Abstract