The axioms listed above primarily work through the deduction metatheorem to arrive at completeness. Here is another axiom system that aims directly at completeness without going through the deduction metatheorem.

First we have axiom schemas that are designed to efficiently prove the subset of tautologies that contain only one propositional variable.
* aa 1: ?A->A
* aa 2: (A->B)->?(A->(C->B))
* aa 3: A->((B->C)->?((A->B)->C))
* aa 4: A->?(B->A)The proof of each such tautology