The following I've learned with the help of the late William McCune's program Prover9 https://www.cs.unm.edu/~mccune/mace4/  2005-2010.

In the following the symbol '0', given a context, stands for a constant false propositions.  The sense behind the idea of '0' thus may get captured by the following sentence:

"When you are awake, The Earth is exactly the same as The Sun."

Suppose we consider the following basis for classical propositional logic.  The small letters for this system only get taken from the second half of the English abc's for small letters.  We might also subscript them with numeral symbols so long as each symbols can get clearly distinguished from other symbols.


1. C x Cyx.  Recursive Meaningful Expression Prefixing

2. C CxCyz C Cxy Cxz.  C-Distribution

3. C CCxy0 x.  Arbitrary Implication to Falsum to the Antecedent of the Implication.

Suppose also we have the following definitions:



def. 1: Nx is defined as Cx0.

def. 2: Axy is defined as CCxyy.

def. 3: Kxy is defined as CCxCy00.

def. 4: Exy is defined as CCCxyCCyx00.

The third axiom along with the above definitions allows us to deduce a few theorems in just a few steps. 

Applying def. 1 to 3. we obtain 4

4 C NCxy x. Negation of an arbitrary conditional to the antecedent of that conditional.

Now putting 0 in the place of y in 4 we obtain 5 (we can abbreviate that as x/0 * 5 following the scheme x/y * z, which I will use hereafter):

5 C NCx0 x.

Applying def. 4 to CNx0 in 5 we obtain 6:

6 C NNx x.  Double negation to the small letter of the meaningful expression.

3 y/Cy0 * 7

7 C CCxCy00 x.

Applying def. 3 to CCxCy00 in 7 we obtain 8:

8 C Kxy x.  Arbitrary conjunction to it's left meaningful expression.

1 y/Cyx * 9

9 C x CCyx x.

Applying def. 2 to CCyxx in 9 we obtain 10:

10 C x Ayx.  Arbitrary proposition to a disjunction with that proposition on the right of the disjunction.

3 x/Cxy, y/CCyx0 * 11

11 C CCCxyCCyx00 Cxy.

Applying def. 4 to CCCxyCCyx00 in 11 we obtain 12:

12 C Exy Cxy.   Arbitrary equivalence to a similar conditional.