7
$\begingroup$

I'm trying to use those Logical equivalence as axioms to prove some PL statements,
In this case I followed the examples in the documentation that didn't use the build-in logic functions$\{\text{And}[,],\text{Or}[,],\text{etc}\}$, the reason is, otherwise it will evaluate some axioms as True.

Here is my code: (Updated)

PL = {ForAll[{p, q, r}, and[p, True] == p],
  ForAll[{p, q, r}, or[p, False] == p],
  ForAll[{p, q, r}, or[p, True] == True],
  ForAll[{p, q, r}, and[p, False] == False],
  ForAll[{p, q, r}, or[p, p] == p],
  ForAll[{p, q, r}, and[p, p] == p],
  ForAll[{p, q, r}, not[not[p]] == p],
  ForAll[{p, q, r}, or[p, q] == or[q, p]],
  ForAll[{p, q, r}, and[p, q] == and[q, p]], 
  ForAll[{p, q, r}, or[or[p, q], r] == or[p, or[q, r]]], 
  ForAll[{p, q, r}, and[and[p, q], r] == and[p, and[q, r]]], 
  ForAll[{p, q, r}, or[p, and[q, r]] == and[or[p, q], or[p, r]]], 
  ForAll[{p, q, r}, and[p, or[q, r]] == or[and[p, q], and[p, r]]], 
  ForAll[{p, q, r}, not[and[p, q]] == or[not[p], not[q]]], 
  ForAll[{p, q, r}, not[or[p, q]] == and[not[p], not[q]]], 
  ForAll[{p, q, r}, or[p, and[p, q]] == p],
  ForAll[{p, q, r}, and[p, or[p, q]] == p],
  ForAll[{p, q, r}, or[p, not[p]] == True],
  ForAll[{p, q, r}, and[p, not[p]] == False]}
proof = FindEquationalProof[
  ForAll[{p, q, r}, 
   and[or[and[and[r, not[q]], not[p]], 
      and[q, not[and[q, not[or[p, r]]]]]], 
     not[and[p, not[and[q, not[r]]]]]] == 
    or[and[and[p, q], not[and[r, q]]], and[r, not[p]]]], PL]
proof["ProofGraph"]
proof["ProofNotebook"]

I just fixed the typo in the axiom, yet trying to let it prove that statement:

$$((r ∧ ¬q ∧ ¬p) ∨ (q ∧ ¬(q ∧ ¬(p ∨ r)))) ∧ ¬(p ∧ ¬(q ∧ ¬r))$$

$$\equiv(p ∧ q ∧ ¬(r ∧ q)) ∨ (r ∧ ¬p)$$

and[or[and[and[r, not[q]], not[p]], 
          and[q, not[and[q, not[or[p, r]]]]]], 
         not[and[p, not[and[q, not[r]]]]]] == 
        or[and[and[p, q], not[and[r, q]]], and[r, not[p]]]], PL]

But seems not work, i tried shorter ones, which works fine, is it because this statement too long or something I missed $?$

However it can be proved with booleanLogic axioms given in documentation, with 402 steps:

booleanLogic = {ForAll[{a, b}, and[a, b] == and[b, a]],
ForAll[{a, b}, or[a, b] == or[b, a]],
ForAll[{a, b}, and[a, or[b, not[b]]] == a],
ForAll[{a, b}, or[a, and[b, not[b]]] == a],
ForAll[{a, b, c}, and[a, or[b, c]] == or[and[a, b], and[a, c]]],
ForAll[{a, b, c}, or[a, and[b, c]] == and[or[a, b], or[a, c]]]}

proof = FindEquationalProof[
  ForAll[{p, q, r}, 
   and[or[and[and[r, not[q]], not[p]], 
      and[q, not[and[q, not[or[p, r]]]]]], 
     not[and[p, not[and[q, not[r]]]]]] == 
    or[and[and[p, q], not[and[r, q]]], and[r, not[p]]]], booleanLogic]
proof["ProofGraph"]
proof["ProofNotebook"]

And here is the proof graph:

Any help would be appreciated.

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ You could build a truth table (true and false) for each value of p, q and r. That might identify any invalid axioms. $\endgroup$
    – mikado
    Commented Nov 9, 2019 at 7:32
  • 2
    $\begingroup$ the third-to-last axiom seems wrong: $\lnot(p\lor q)\equiv\lnot p\lor\lnot q$ should be $\lnot(p\lor q)\equiv\lnot p\land\lnot q$ $\endgroup$
    – Lukas Lang
    Commented Nov 9, 2019 at 15:48
  • $\begingroup$ @LukasLang Thanks! $\endgroup$
    – Ethan
    Commented Nov 9, 2019 at 17:17
  • 1
    $\begingroup$ I think True and False in your axioms make problems. Try to replace these by T and F. My comp is too weak to realize my suggestion (so does my Mathematica Online). $\endgroup$
    – user64494
    Commented Dec 15, 2019 at 7:57
  • $\begingroup$ @user64494 My free online cloud can't run it too $\dots$ but I tried use it to prove two Consensus theorems, where Identity, Domination, Negation laws play a important roles in the proof: \begin{align} &\text{1. or[or[and[x,y],and[not[x],z]],and[y,z]]==or[and[x,y],and[not[x],z]]]}\\ &\text{2. and[and[or[x,y],or[not[x],z]],or[y,z]]==and[or[x,y],or[not[x],z]]}\\ \end{align} and both axiom works, use True, Flase seems make no difference from T,F, but thanks for the suggestion. $\endgroup$
    – Ethan
    Commented Dec 17, 2019 at 23:38

1 Answer 1

Reset to default
1
$\begingroup$

The first four axioms are provably redundant; removing them creates a system that works. 

PL2 = {ForAll[{p, q, r}, or[p, p] == p],
  ForAll[{p, q, r}, and[p, p] == p],
  ForAll[{p, q, r}, not[not[p]] == p],
  ForAll[{p, q, r}, or[p, q] == or[q, p]],
  ForAll[{p, q, r}, and[p, q] == and[q, p]],
  ForAll[{p, q, r}, or[or[p, q], r] == or[p, or[q, r]]],
  ForAll[{p, q, r}, and[and[p, q], r] == and[p, and[q, r]]],
  ForAll[{p, q, r}, or[p, and[q, r]] == and[or[p, q], or[p, r]]],
  ForAll[{p, q, r}, and[p, or[q, r]] == or[and[p, q], and[p, r]]],
  ForAll[{p, q, r}, not[and[p, q]] == or[not[p], not[q]]],
  ForAll[{p, q, r}, not[or[p, q]] == and[not[p], not[q]]],
  ForAll[{p, q, r}, or[p, and[p, q]] == p],
  ForAll[{p, q, r}, and[p, or[p, q]] == p],
  ForAll[{p, q, r}, or[p, not[p]] == True],
  ForAll[{p, q, r}, and[p, not[p]] == False]}
proof = FindEquationalProof[
  ForAll[{p, q, r}, 
   and[or[and[and[r, not[q]], not[p]], 
      and[q, not[and[q, not[or[p, r]]]]]], 
     not[and[p, not[and[q, not[r]]]]]] == 
    or[and[and[p, q], not[and[r, q]]], and[r, not[p]]]], PL2]
proof["ProofGraph"]
proof["ProofNotebook"]
Improve this answer
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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