Formula of the Day: CδCpqδANpq.

"δ" in opposition to representing a propositional variable indicates a functorial variable of arity one.  In other words, it stands for any of the unary functions presumed.  Given the context of classical logic this means it stands for any of the functions belonging to {F, N, I, V} where F(0)=0, F(1)=0, N(0)=1, N(1)=0, I(0)=0, I(1)=1, V(0)=1, V(1).  Thus we can check that CδCpqδANpq constitutes a tautology by checking that each member of {CFCpqFANpq, CNCpqNANpq, CICpqIANpq, CVCpqVANpq} is a tautology in 2-valued logic.

In notation for substitution for δ, an apostrophe " ' " means that we substitute the argument that follows delta for the apostrophe.  For example, from 1 δp, 1 δ/C'q we substitute δ with C, then the argument that follows δ which is "p" in this case, and then "q" obtaining Cpq.  If we write 2 CsδCpCqr, 2 δ/C'' that means we substitute δ with C, then the argument of δ CpCqr, then the argument of δ CpCqr obtaining CsCCpCqrCpCqr.  If we write 3 CpCCpδqr, 3 δ/CC'r' then we write CC, the argument of δ q, r, and lastly the argument of δ "q" again in place of δq obtaining CpCCpCCqrqr.  δ/' just means we substitute δ with the argument of δ.
CδCpqδANpq can effectively take the place of a definition of the conditional "C" in a logical calculus.  Let's consider CδCpqδANpq in the following system:

axiom                     1 ApNp
axiom                     2 CδCpqδANpq
2 δ/CCδCpqδ'CδANpqδCpq    3 CCCδCpqδCpqCδANpqδCpqCCδCpqδANpqCδANpqδCpq
2 δ/Cδ'δCpq               4 CCδCpqδCpqCδANpqδCpq
D3.4                      5 CCδCpqδANpqCδANpqδCpq
D5.2                      6 CδANpqδCpq
6 δ/'                     7 CANpqCpq
D7.1                      8 CpNNp

Thus, double negation introduction CpNNp follows from these two axioms.  It also follows that in the presence of a definition corresponding to axiom 2, the law of the excluded middle ApNp allows us to derive the law of double negation introduction CpNNp.