001 Commutative Laws in Logic
Commutative Equivalences in Logic
\[p \wedge q \equiv q \wedge p,\]
\[p \vee q \equiv q \vee p.\]
Examples
Let p: "The number \(n\) is natural.", and q: "The number \(n\) is even."
Conjunction
“The number \(n\) is natural and even” is logically equivalent to “The number \(n\) is even and natural.”
Disjunction
“The number \(n\) is natural or even” is logically equivalent to “The number \(n\) is even or natural.”
Meaning of the used symbols
| Symbol | Meaning |
|---|---|
| \(\equiv\) | is logically equivalent to |
| \(\wedge\) | and |
| \(\vee\) | (not exclusive) or |
Formal verification in Lean
You can find the formal verification of the commutative laws in logic in Lean in this GitHub repository. The code rigorously proves that the order of operands in logical conjunction and disjunction does not affect the outcome, demonstrating these fundamental properties within a formal proof assistant environment.