Formula of the Day: The law of commutation CCpCqrCqCpr.

If we look at CCpCqrCqCpr it turns out that we can obtain the consequent implying the antecedent just from substitution.  Let X p/a indicate that variable p gets substituted with a throughout formula X.

axiom  1 CCpCqrCqCpr
1 p/a    2 CCaCqrCqCar
2 q/p    3 CCaCprCpCar
3 a/q    4 CCqCprCpCqr

Or if we allow simultaneous substitution in a formula we can proceed as follows:

axiom       1 CCpCqrCqCpr
1 p/q, q/p  2 CCqCprCpCqr

The law of commutation, unlike the law of identity, can also serve as the sole axiom of a system under detachment, and from it as an axiom we can obtain well-formed formulas (or "formulas") which are not substitution instances of it (unlike Cpp as the sole axiom of a system).

axiom  1 CCpCqrCqCpr
D1.1    2 CpCCqCprCqr
D2.2    3 CCpCCqCCrCqsCrstCpt
D2.1    4 CCpCCCqCrsCrCqstCpt
D1.4    5 CpCCpCCCqCrsCrCqstt
D1.3    6 CpCCpCCqCCrCqsCrstt
D2.3    7 CCuCCCpCCqCCrCqsCrstCptvCuv
D2.7    8 CCwCCCuCCCpCCqCCrCqsCrstCptvCuvyCwy
D2.8    9 CCzCCCwCCCuCCCpCCqCCrCqsCrstCptvCuvyCwyaCza

The system {CCpCqrCqCpr} has no last most general theorem, as can get understood from theorem 2 CpCCqCprCqr.  D2.x will always yield a theorem, since any variable can get substituted by any theorem, and CCqCprCqr where p is any theorem is a well-formed formula.  Thus, D2.2 yields a theorem.  D2.D2.2 yields a theorem.  D2.D2.D2.2 yields a theorem and so on.  Each theorem has more symbols than the last theorem also, since the antecedent "p" appears in the consequent of CpCCqCprCqr, and since every theorem has more symbols than Cp, the detached theorem having the form CCqCprCqr will have more letters than the theorem that served as the major premise.  Theorems 5, and 6 also indicate that there exist subsystems of CCpCqrCqCpr which like the subsystem {CpCCqCprCqr} have no last most general theorem.

The law of commutation appeared in the first axiom system for propositional calculus ever proposed.  Gottlob Frege's system was {CpCqp, CCpCqrCCpqCpr, CCpCqrCqCpr, CNNpp, CpNNp, CCpqCNqNp}.  Jan Lukasiewicz figured out that the law of commutation could get derived from the first two axioms a few decades later.  Here's a proof:

axiom   1 CpCqp
axiom   2 CCpCqrCCpqCpr
D1.2     3 CpCCqCrsCCqrCqs
D2.3     4 CCpCqCrsCpCCqrCqs
D1.4     5 CpCCqCrCstCqCCrsCrt
D2.5     6 CCpCqCrCstCpCqCCrsCrt
D6.1     7 CCpCqrCsCCpqCpr
D4.7     8 CCpCqrCCsCpqCsCpr
D2.8     9 CCCpCqrCsCpqCCpCqrCsCpr
D1.1   10 CpCqCrq
D9.10 11 CCpCqrCqCpr

The law of commutation also appears as an axiom or theorem in many other systems of logic.  If one has it in a system S, and it does NOT need one of the axioms to get derived, then there may very well exist a way to figure out an alternative system A which has the same theorems as S.  For instance, we'll start by pointing out that CCpCqrCqCpr comes as derivable from {CpCqp, CCpCqrCCpqCpr} above.  Now since CCpqCNqNp and D [CCpCqrCCpqCpr].[CCpqCNqNp] exists it turns out that the theorems of Frege's system have another axiomization than {CpCqp, CCpCqrCCpqCpr, CNNpp, CpNNp, 5a-CCpqCNqNp}.  Namely, that axiomization is {CpCqp, CCpCqrCCpqCpr, CNNpp, CpNNp, 5b-CNpCCqpNq}.  To prove this we only need to write out that D[ CCpCqrCqCpr].5a yields 5b and D[CCpCqrCqCpr].5b yields 5a.

Also, let's suppose that we have CCpCqrCqCpr and Cpp as our axioms:

axiom   1  CCpCqrCqCpr
axiom   2  Cpp
D1.2     3  CpCCpqq
D3.2     4  CCCppqq
D1.4     5  CpCCCqqCprr
D1.5     6  CCCppCqrCqr

Notice that 6 is not the same formula as 4, but 6 is a more specialized (or less general) formula than 4 since we can obtain 6 from 4 by substitution only.