 In the examples below, each formula number is followed first by Principia notation and then its modern translation. Notice that in ∗1·5 parentheses are used for punctuation in addition to dots. (Primitive Propositions ∗1·2, ∗1·3, ∗1·4, ∗1·5, and ∗1·6 together constitute the axioms for propositional logic in PM.) Proposition ∗1·5 was shown to be redundant by Paul Bernays in 1926. It can be derived from appropriate instances of the others and the rule of modus ponens.