Interested in a "more fundamental" proof for basic properties of the logical connectives

Question

Starting with the classical propositional logic, is there a rather canonical way to prove that $$p\wedge q=q\wedge p$$ for the commutativity of the conjunction and analogously for the other properties and connectives, other than using truth tables, visualizing with Venn diagrams akin Wikipedia's approach, or verbal philosophical reasoning?

Put it other way, can we well-define the connectives from a deeper foundation than that?

For example, in set theory, we define a union of the two sets $A$, $B$ as $$A\cap B:=\{x\,|\,x\in A\wedge x\in B\}$$ to then move on and prove that $\cap$ is commutative. By doing so we simply delegate the proof to the very propositional (or whichever) logic we defined the operator with $$A\cap B\overset{\mathrm{def}}{=}\{x\,|\,x\in A\wedge x\in B\}\overset{\mathrm{com}}{=}\{x\,|\,x\in B\wedge x\in A\}\overset{\mathrm{def}}{=}B\cap A.\square$$

Answer 1

I'm not sure this will satisfy you, but a categorically-minded way to characterize meets $a \wedge b$ and joins $a \vee b$ is via universal properties:

$$x \leq a \wedge b \;\;\; \text{iff}\;\;\; x \leq a,\; x \leq b$$

$$a \vee b \leq x\;\;\; \text{iff}\;\;\; a \leq x,\; b \leq x$$

for any $x$. These are general definitions in the theory of posets or preorders, but for propositions, we can think of $\leq$ as denoting the entailment relation. The pair of entailments on the right (for each of $\wedge, \vee$) simply means both are asserted.

In that case, one can prove $a \wedge b = b \wedge a$. For, we have

$$x \leq a \wedge b\;\;\; \text{iff}\;\;\; x \leq a, x \leq b\;\;\; \text{iff}\;\;\; x \leq b \wedge a.$$

Now, since $a \wedge b \leq a \wedge b$, we can put $x = a \wedge b$ and reason forward to conclude $a \wedge b \leq b \wedge a$. Similarly, putting $x = b \wedge a$ and reasoning backward, we conclude $b \wedge a \leq a \wedge b$. Thus, if we take propositions to be equal if they entail one another (i.e., if we assume the antisymmetry axiom for posets), we derive $a \wedge b = b \wedge a$. Similarly we can prove $a \vee b = b \vee a$.

A similar "universality argument" can be used to prove that $\wedge, \vee$ are associative, idempotent, etc.

Once we have universal characterizations for $\wedge, \vee$, we can add a third that characterizes negation

$$a \wedge b \leq c\;\;\; \text{iff}\;\;\; a \leq (\neg b) \vee c$$

and in this way we get classical propositional logic (more exactly, we'd add in two more to characterize the top element $\top$ ("true") and $\bot$ ("false")).

Answer 2

Once you select a particular proof system, you should be able to write down a formal proof of $(p\land q)\leftrightarrow (q \land p)$. How such a proof will look will vary wildly between different proof systems, though.

For example, in (classical or intuitionistic) sequent calulus, the formal proof might look like this: $$ \begin{array}{rll} 1) & q \vdash q & \text{axiom} \\ 2) & p,q \vdash q & 1, \text{weakening} \\ 3) & p \vdash p & \text{axiom} \\ 4) & p,q \vdash p & 3, \text{weakening} \\ 5) & p,q \vdash q\land p & 2,4,{\land}\mathrm I \\ 6) & p\land q \vdash q \land p & 5, {\land}\mathrm E \\ 7) & \vdash (p\land q) \to (q\land p) & 6, {\to}\mathrm I \\ 8-14) & \vdash (q\land p) \to (p\land q) & \text{(repeat the above with $p$ and $q$ interchanged)} \\ 15 & \vdash (p\land q) \leftrightarrow (q\land p) & 7, 14, {\leftrightarrow}I \end{array} $$

However, such a proof doesn't really offer any deep insight into how conjunction works. It says more about the proof system than about conjunction, namely that the proof system works "in a sane way" with respect to conjunction.

If you're not interested in proof systems, but in semantics, then you don't get around the fact that truth tables is the most fundamental way to define the semantics of the propositional connectives -- much more suitable as a definition than verbal descriptions. Therefore a truth-table based proof is the most fundamental proof you can possibly get about semantics here, and everything else will just be more or less convincingly paraphrased guises for the fundamental truth-table based proof.