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$ 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$ Commented Nov 9, 2019 at 15:48
  • $\begingroup$ @LukasLang Thanks! $\endgroup$ 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$ 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$ 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

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.