 In this section we will use A, B, etc as meta-linguistic variables for formulas. The formulas constructed from atomic propositions with the connectives are said to express elementary propositions to distinguish them from propositions involving quantifiers and propositional functions. The system is organized axiomatically, the axioms, called “primitive propositions” or “Pp”, are presented with the characteristic ‘\(\supset\)’ of material implication, which is defined with \(\lnot\) and \(\lor\). The connectives \(\amp\) and \(\equiv\) are also defined, but not needed in the statements of the axioms. This peculiarity has its origins in Russell’s view from 1903 that 