Well-Formed Formula of the Day: ApNp

ApNp consists of a symbolic formulation of the law of the excluded middle "either a proposition is true or it is not true."  If we wanted to use at as an axiom, we might want to have as a deduction rule {ANpq, p}->q, but even then we'd probably want to commute ApNp and use ANpp instead.  Let's say we have ANpp as an axiom along with ANpANqp as an axiom.  We might proceed as follows.

axiom  1 ANpp
axiom  2 ANpANqp
D2.2    3 ANpANqANrq
D2.1    4 ANpANqq

ApNp can get proved from the axiom set {CpCqp, CCpCqrCCpqCpr, CCNpqCCNpNqp, CpApq, CpAqp}.  ApNp is unique among classical logic theorems which only have C, A, K, E, and N as connectives in them in that it has exactly 4 symbols.