2
$\begingroup$

As part of the proof of a proposition in an economics paper, I need to show that a system of inequalities in four variables is inconsistent. Because the system is complicated, I cannot show this analytically. However, Reduce[System,{x1, x2, x3, x4}, Reals] returns False. Is it acceptable to use this result as part of the formal proof of my proposition? That is, is the algorithm that Reduce uses exact? Or does it use short-cuts, approximations, etc.?

$\endgroup$
  • $\begingroup$ It is certainly a verification if you accept that Reduce has no bugs that are affecting its evaluation of your inequalities. Whether or not citing the results in a paper will be accepted, is a something the journal editor will decide. It is not an issue for this site. $\endgroup$ – m_goldberg Jul 20 '17 at 15:04
4
$\begingroup$

Is it acceptable to use this result as part of the formal proof of my proposition?

In general, no... Mathematica has bugs and problems with differences between its interpretation of things vs. what users may expect. A better approach would be to post the equations or describe them to see what form they take and find out if anyone knows a way to prove they're inconsistent. For instance, it's entirely possible someone may know what algorithm Reduce will use to prove your inequalities, and you may be able to reproduce what it does in more straightforwardly provable steps.

$\endgroup$
  • $\begingroup$ Thanks. I guess my question can be broken down into: A) Is Reduce meant to be exact? and B) Are bugs impossible or at least no more likely than mistakes in existing theorems that one can invoke in a proof? Anything other than "Yes" on both question means that I cannot use the results of Reduce in a formal proof. I think you are saying that the answer is "No" to the second question. As to posting the inequalities: There are several systems and many of them involve long, complicated expressions. I don't think I can expect anyone to wade through them. And there's probably no magic trick. $\endgroup$ – Asen Ivanov Jul 21 '17 at 18:43

Not the answer you're looking for? Browse other questions tagged or ask your own question.