I am currently a math student in cal $b$. I know a super intelligent person that is trying to teach me symbolic logic. We've been doing okay until we've hit associativity. My "teacher" (the intelligent one) said it wasn't proved in his class and he's never seen a proof for it (that doesn't use demorgans laws). I'd love to see a proof without using DeMorgan's laws.

So If anyone knows it here's what I'd like to see.

Prove $pv(qvr)\Rightarrow(pvq)vr$

I have most of the basic theorems and such including commutivity and the contrapositive proved, but no DeMorgan's.

Thanks guys, Have fun!!

  • $\begingroup$ A truth table will clinch it. Boring, but not too hard (only 8 rows), and guaranteed to work. $\endgroup$
    – quasi
    Mar 22 '17 at 0:08
  • $\begingroup$ It would be interesting to see a proof tree for this. $\endgroup$ Mar 22 '17 at 0:13
  • 1
    $\begingroup$ Isn't associativity an axiom of propositional logic? $\endgroup$ Mar 22 '17 at 1:09
  • $\begingroup$ I have no idea why you would think DeMorgan would even help with this ... Anyway, a basic truth-table will do the trick. $\endgroup$
    – Bram28
    Mar 22 '17 at 1:09
  • $\begingroup$ @Bram28, If you're studying a formal deduction system (e.g. Natural Deduction) then it's not trivial at all that truth tables would give the same results. (See some discussion on wikipedia here.) $\endgroup$
    – Mark S.
    Mar 22 '17 at 2:17

To prove $p\lor(q\lor r)$ implies $(p\lor q)\lor r$, assume $p\lor(q\lor r)$ is true, and then, using that assumption, show that $(p\lor q)\lor r$ is true.

Thus, assume $p\lor(q\lor r)$ is true.

Then $p$ is true, or $q \lor r$ is true.

Suppose first that $p$ is true.

Then the truth of $p$ implies the truth of $p \lor q$, which in turn implies the truth of $(p\lor q)\lor r$, as required, so this case is done.

Next suppose $q \lor r$ is true.

Consider two subcases ...

Suppose first that $q\,$ is true

Can you finish it?


The OP has not specified what sort of deduction system they're using (natural deduction?), a computer-verified proof is available at this page on Metamath.

Basically, the proof steps are:

  1. A tautology version of disjunction introduction lets us write $\varphi\to(\varphi\lor\chi)$
  2. An "in the consequent" version allows us to introduce $\psi$ to the above to get $\varphi\to\left(\psi\lor(\varphi\lor\chi)\right)$
  3. The other tautology version lets us write $\chi\to(\varphi\lor\chi)$
  4. An "on both sides" version allows us to introduce $\psi$ to both sides of the above to get $(\psi\lor\chi)\to\left(\psi\lor(\varphi\lor\chi)\right)$
  5. Finally, a theorem about combining two different implications with disjunction of the antecedents lets us take the things from lines 2 and 4 to get the desired $\left(\varphi\lor(\psi\lor\chi)\right)\to\left(\psi\lor(\varphi\lor\chi)\right)$

This proof and its required theorems have been verified in a certain system with only a few axioms discovered by Jan Łukasiewicz (Wikipedia's explanation, Metamath's explanation). The proof ultimately relies on a list of things* that are all numbered less than 400 except for orim12i #504 and orim2i #506. Since DeMorgan's laws are #476, #477, #478, and #484, this proof doesn't use DeMorgan's laws.

*Unfortunately, it's not feasible (certainly not readable) to reproduce the entire tree down to the axioms, but I can list what is used. Specifically, the proof relies on: the four syntax definitions that say its valid to use logical symbols (negations, implications, biconditionals, and disjunctions), the axioms and deduction rule (Simp, Frege, Transp., and Modus Ponens), the definition of or in terms of negation and implication, and the following 63 theorems:

$\begin{matrix} \text{a1i}&\text{mpdd}&\text{con1i}&\text{sylbi}\\ \text{a2i}&\text{pm2.43i}&\text{con3d}&\text{bi2}\\ \text{mpd}&\text{syl6c}&\text{con3rr3}&\text{bicom1}\\ \text{syl}&\text{con4d}&\text{pm3.2im}&\text{bicomi}\\ \text{mpi}&\text{pm2.21d}&\text{impi}&\text{biimpri}\\ \text{mp2}&\text{pm2.21}&\text{expi}&\text{pm2.53}\\ \text{id}&\text{pm2.24}&\text{simprim}&\text{pm2.54}\\ \text{idd}&\text{notnot2}&\text{simplim}&\text{orrd}\\ \text{a1d}&\text{con2d}&\text{bi1}&\text{jaoi}\\ \text{a2d}&\text{mt2d}&\text{bi3}&\text{olc}\\ \text{sylcom}&\text{nsyl3}&\text{impbii}&\text{orc}\\ \text{syl5com}&\text{con2i}&\text{impbidd}&\text{orcd}\\ \text{com12}&\text{notnot1}&\text{impbid21d}&\text{olcd}\\ \text{syl5}&\text{con1d}&\text{impbid}&\text{orim12i}\\ \text{syl6}&\text{mt3d}&\text{dfbi1}&\text{orim2i}\\ \text{pm2.27}&\text{nsyl2}&\text{biimpi}&\text{}\\ \end{matrix}$


From your question it is not clear what kind of proof you are looking for, so I will give a couple of different proofs.

First, a formal semantical one. That is, using the basic truth-functional definition of $\lor$:

$p \lor (q \lor r)$ is false iff

both $p$ and $q \lor r$ are false iff

$p$, $q$, and $r$ are all false iff

both $p \lor q$ and $q$ are false iff

$(p \lor q) \lor r$ is false

This of course also means that $p \lor (q \lor r)$ is true iff $(p \lor q) \lor r$ is true. Hence, they are equivalent.

Second, a formal derivation or formal proof. Now, there are many different proof systems, so if you were looking for one of these, you should have specified the inference rules that would be allowed, but in the absence of that, here is a formal derivation style proof in a fairly standard Fitch-style natural deduction type formal proof:

enter image description here

Finally, given your comment not to use DeMorgan, I suspect that you are looking for an algebraic proof. Now again, that means that you will have to tell us what equivalences we are allowed to use, but let's assume the following fairly standard equivalences:


$p \land q \Leftrightarrow q \land p$

$p \lor q \Leftrightarrow q \lor p$

Double Negation

$\neg \neg p \Leftrightarrow p$


$p \rightarrow q \Leftrightarrow \neg p \lor q$


$p \rightarrow (q \rightarrow r) \Leftrightarrow (p \land q) \rightarrow r$

With these, you can do the following:

$p \lor (q \lor r) \Leftrightarrow$ (Commutation)

$p \lor (r \lor q) \Leftrightarrow$ (Double Negation x 2)

$\neg \neg p \lor (\neg \neg r \lor q) \Leftrightarrow$ (Implication x 2)

$\neg p \rightarrow (\neg r \rightarrow q) \Leftrightarrow$ (Exportation)

$(\neg p \land \neg r) \rightarrow q) \Leftrightarrow$ (Commutation)

$(\neg r \land \neg p) \rightarrow q) \Leftrightarrow$ (Exportation)

$\neg r \rightarrow (\neg p \rightarrow q) \Leftrightarrow$ (Implication x 2)

$\neg \neg r \lor (\neg \neg p \lor q) \Leftrightarrow$ (Double Negation x 2)

$r \lor (p \lor q) \Leftrightarrow$ (Commutation)

$(p \lor q) \lor r$


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