# FindEquationalProof with Logic in Wolfram Mathematica

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??

• What does the documentation say? The message you’re getting makes it pretty clear you’re not specifying your arguments correctly – b3m2a1 Jan 7 '19 at 2:14
• ForAll[{a, b}, Implies[a, b]] doesn't really make sense though. It says that anything implies anything else. – Szabolcs Jan 7 '19 at 11:05
• The examples in the docs seem to have equations -- since it's in the name, it's probably important. – Michael E2 Jan 7 '19 at 18:09
• 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? – Michael E2 Jan 7 '19 at 18:12
• @MichaelE2 Yeah! I looking for ProofObject – 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]]];
Resolve[%]


True

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.