 All of the “primitive propositions” of PoM are stated with only material implication as a primitive connective. The connectives \(\amp\),\(\lor\) and \(\equiv\), are defined as might be expected. The notion of negation, expressed by \(\lnot\), is defined using a notion of quantification over propositions ( \(\lnot A\) means that A implies all propositions). By 1906 Russell had decided to use \(\lnot\) as a primitive connective, and no longer used propositional quantifiers, allowing \(\supset\) to be defined, while the primitive propositions were still stated with \(\supset\) and \(\lor\). That the system of propositional logic in PM was the result of an evolution of changes in choices of primitives is mirrored in the choice of theorems that are proved in the first chapters. While most are proved because they will be used later in PM, some remain simply as remants of the earlier systems. In particular PM contains several theorems that were primitive propositions in earlier systems, though not used in what follows. In fact one primitive proposition of PoM, known as “Peirce’s Law (\([(p \supset q )\supset p ] \supset p\)) appears to have been proved in an early version of PM as ∗2·7 but simply deleted (and its number not reassigned to another theorem) simply to save space (see Linsky 2016).