I try to "make" proof in Wolfram Mathematica.

Thats a proof:

if a->b and b->c then a->c

I tried

bl = {ForAll[{a, b}, Implies[a, b]], ForAll[{b, c}, Implies[b, c]]}
proof = FindEquationalProof[ForAll[{a, c}, Implies[a, c]], bl]

but it say:

FindEquationalProof::invs: Invalid specification of propositions ... and axioms ...

How i can solve this problem??

  • 1
    $\begingroup$ What does the documentation say? The message you’re getting makes it pretty clear you’re not specifying your arguments correctly $\endgroup$ – b3m2a1 Jan 7 '19 at 2:14
  • $\begingroup$ ForAll[{a, b}, Implies[a, b]] doesn't really make sense though. It says that anything implies anything else. $\endgroup$ – Szabolcs Jan 7 '19 at 11:05
  • 1
    $\begingroup$ The examples in the docs seem to have equations -- since it's in the name, it's probably important. $\endgroup$ – Michael E2 Jan 7 '19 at 18:09
  • 1
    $\begingroup$ I take it that the idea is to construct a ProofObject for this proposition, not merely to get Mathematica to tell you it's true. Is that correct? $\endgroup$ – Michael E2 Jan 7 '19 at 18:12
  • 2
    $\begingroup$ @MichaelE2 Yeah! I looking for ProofObject $\endgroup$ – J.A.B. Jan 8 '19 at 18:28

You don't need FindEquationalProof to this end, it is enough to use the quantifiers.

ForAll[{a, b, c}, Implies[Implies[a, b] && Implies[b, c], Implies[a, c]]];


See Mathematica help for more info. If you insist to use FindEquationalProof here, then you may apply the following axioms of propositional logic

shefferLogic = {ForAll[a, nand[nand[a, a], nand[a, a]] == a],
ForAll[{a, b}, nand[a, nand[b, nand[b, b]]] == nand[a, a]],
ForAll[{a, b, c},  nand[nand[a, nand[b, c]], nand[a, nand[b, c]]] == 
nand[nand[nand[b, b], a], nand[nand[c, c], a]]]}

, reformulating your theorem in terms of the Sheffer stroke. Good luck!

Addition. One more way to prove it is to check whether the formula defines tautology.

BooleanTable[ Implies[Implies[a, b] && Implies[b, c], Implies[a, c]], {a, b, c}]

{True, True, True, True, True, True, True, True}

It should be noticed that the formula under consideration is taken as an axiom in some systems of axioms of propositional calculus. See Wiki for more info.

| improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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