File 20180912_AllBoolean_eqvs.pdf is a monograph of extensively automated proofs (implemented in Mathematica) of the implicational equivalence of equational Boolean, Huntington, Robbins, Sheffer, and two Wolfram logics. The derivations include what appears to be a novel proof of the Robbins conjecture (“A Robbins logic is a Boolean logic”).
Mathematica v12.1.0, released March 2020, contains an enhancement of Mathematica’s equational-logic proof search function FindEquationalProof. The enhancement automatically converts Mathematica first-order predicate logic expressions to equational logic (prior versions did not provide this conversion). The v12.1.0 distribution contains an example (Lewis Carroll’s Puzzle Number 1 (1896) showcasing the conversion capability. The example proves that “Babies can’t manage crocodiles”, given:
(a) All babies are illogical.
(b) Nobody is despised who can manage a crocodile.
(c) Illogical persons are despised.
I made minor modifications to the example provided in the Wolfram distribution; the results are shown here.
In a scene in Letters from the Earth (Twain 1962, “Extract from Eve’s Diary”, 82), Adam and Eve stand in the Garden of Eden some distance from the First Lion — “William McKinley” — discussing whether McKinley is a vegetarian. Adam propounds a long-winded, first-principles argument for the claim,
concluding that the First Lion eats no meat.
Eve, who had seen McKinley devour the First Lamb just a few days earlier, counters, “Adam, I think there is something better than logic.”
“And what could that be?” he asks.
“Fact”, she replies.
Adam’s argument is in some ways akin to some of Lewis Carroll’s “Logical Puzzles” (1896), which trade on contrapositive inference. Here, I use the automated deduction functionality in Mathematica (2020) to produce an equational logic proof of a variant of Adam’s argument.
Click Lions Eat Only Strawberries to see the proof.
———-
Carroll L. (1896). Symbolic Logic. Reprinted by Clarkson N.Potter, 1977.
Twain M. (1962). Letters From the Earth. B. DeVoto (ed.) Harper and Row.
Wolfram Research (2020). Mathematica v12 .1 .0 Home Edition.
https : // www.wolfram.com/mathematica – home – edition /. Accessed 19 March 2020.
Click here for a Mathematica-based automated equational logic derivation of the implicational equivalence of Lukasiewicz’s CN and the Principia Mathmatica sentential calculi.
Click here for a Mathematica-based automated equational logic derivation of Exercise 60 (“I avoid kangaroos”) of Lewis Carroll’s Symbolic Logic.