Proving propositional logic associativity with natural deduction

Question

I'm pretty sure similar question was asked, so sorry that I'm posting this again, but just reading the answers on that question didn't seem to provide enough insight for me and I'd just like to double-check if I'm getting this right and doing it correctly. Basically I have some info on natural deduction and one example:

Aim to show: $$\begin{align} &p\land q \vdash q \land p \\ &1. p \land q - premise \\ &2. p - \land e_1 \ 1\\ &3. q - \land e_2 \ 1\\ &4. q \land p - \land i \ \ 3,2 \\ \end{align}$$

So as I understand, I can assume that p and q are true and following the elimination rules first eliminate them (p in 2nd line by elimination 1st rule, q in 3rd line by elimination 2nd rule) and then again by the same assumption they're true I can introduce $ \land $ and make $ q \land p $ in the 4th line from 3rd and 2nd line. I don't know if I at least sort of get it or I'm way off, but I've tried to do another example (it has no solution example) and if someone wouldn't mind, I'd like to ask if I got it right, so here's another example:

Aim to show: $$\begin{align} &p \land (q \land r) \vdash (p \land q) \land r \\ &1. p \land (q \land r) - premise \\ &2. p - \land e_1 \ 1 \\ &3. q \land r - \land e_2 \ 1 \\ &4. q - \land e_1 \ 3 \\ &5. r - \land e_2 \ 3 \\ &6. p \land q - \land i \ 2,4 \\ &8. (p \land q) \land r - \land i \ 6,5 \\ \end{align}$$

Is this correct or not? Since proving by natural deduction seems a bit weird for me, compared to all other stuff that I've been doing and I don't know if I get it at least half right.

Answer 1

Natural deduction isn't meant to be weird -- it is meant to be an application of rules of inference that mimics natural language reasoning .

The symbols $p\wedge q$ means that $p$ and $q$ are true.   That $q$ and $p$ are true is represented by the symbols $q\wedge p$.   Therefore: from $p\wedge q$ we may infer $q\wedge p$.   That is $p\wedge q\vdash q\wedge p$

Hence: $~~\bbox[lemonchiffon]{\begin{array}{|lr}1.~ p\wedge q &\textsf{premise}\\\hline 2.~ p & 1, \wedge\mathsf e_1\\ 3.~ q & 1, \wedge\mathsf e_2\\4.~ q\wedge p & 3,2,\wedge \mathsf i\end{array}}$ and similarly : $~~\bbox[lemonchiffon]{\begin{array}{|lr}1.~ p\wedge (q\wedge r) &\textsf{premise}\\\hline 2.~ p & 1, \wedge\mathsf e_1\\ 3.~ q\wedge r & 1, \wedge\mathsf e_2\\4.~ q & 3\wedge \mathsf e_1\\5. ~r& 3,\wedge\mathsf e_2\\6.~ p\wedge q& 2,4\wedge\mathsf i\\7.~(p\wedge q)\wedge r& 6,5,\wedge \mathsf i\end{array}}$ as you derived.

But, anyway, the reason proving commutation and association this way might seem weird is that we expect that of course "and" is associative and commutative.   Why do we have to prove it?

Well, what we are actually proving is that the symbol $\wedge$ is given those properties by the rules of inference $\{\wedge\mathsf e_1, \wedge\mathsf e_2,\wedge\mathsf i\}$, as is necessary for it to represents "and".   So showing that the rules are working as intended (for this, at least).

Answer 2

To verify formal proofs to work you need to check that two states of affairs hold:

1. Every step of the purported proof is well-formed. This doesn't hold for your examples, but I believe it isn't relevant to your question.
2. Every step of the purported proof works out as permissible under the rules of inference.

Again, 2. pretty much only matters for your question. Or at least, I think you would have the same question if you had only printed well-formed formulas. This is where a proof analysis, that is the rightmost column of what you wrote, can help.

So, looking at your example, first we can ask whether or not p∧(q∧r) a permissible premise? Then, does 'p' follow from 1 by the use of rule $$∧e_1$$?

Then we do the same for every other step.

If one step does not satisfy 1. and 2., then the proof as a whole lacks a little bit formally speaking. If every step satisfies 1. and 2., then what gets written in the center column qualifies as a proof.