p ∨ q .⊃. p ∨ r. Pp principle of summation✸1.7. If p is an elementary proposition, ~p is an elementary proposition. Pp✸1.71. If p and q are elementary propositions, p ∨ q is an elementary proposition. Pp✸1.72. If φp and ψp are elementary propositional functions which take elementary propositions as arguments, φp ∨ ψp is an elementary proposition. PpTogether with the "Introduction to the Second Edition", the second edition's Appendix A abandons the entire section ✸9. This includes six primitive propositions ✸9 through ✸9.15 together with the Axioms of reducibility. The revised theory is made difficult by the introduction of the Sheffer stroke ("|") to symbolise "incompatibility" (i.e., if both elementary propositions p and q are true, their "stroke" p | q is false), the contemporary logical NAND (not-AND). In the revised theory, the Introduction presents the notion of "atomic proposition", a "datum" that "belongs to the philosophical part of logic". These have no parts that are propositions and do not contain the notions "all" or "some". For example: "this is red", or "this is earlier than that". Such things can exist ad finitum, i.e., even an "infinite enumeration" of them to replace "generality" (i.e., the notion of "for all"). PM then "advance[s] to molecular propositions" that are all linked by "the stroke". Definitions give equivalences for "~", "∨", "⊃", and ".". The new introduction defines "elementary propositions" as atomic and molecular positions together. It then replaces all the primitive propositions ✸1.2 to ✸1.72 with a single primitive proposition framed in terms of the stroke: "If p, q, r are elementary propositions, given p and p|(q|r), we can infer r. This is a primitive proposition." The new introduction keeps the notation for "there exists" (now recast as "sometimes true") and "for all" (recast as "always true"). Appendix A strengthens the notion of "matrix" or "predicative function" (a "primitive idea", PM 1962:164) and presents four new Primitive propositions as ✸8.1–✸8.13.✸88. Multiplicative axiom✸120. Axiom of infinity Ramified types and the axiom of reducibility In simple type theory objects are elements of various disjoint "types". Types are implicitly built up as follows. If τ1,...,τm are types then there is a type (τ1,...,τm) that can be thought of as the class of propositional functions of τ1,...,τm (which in set theory is essentially the set of subsets of τ1×...×τm). In particular there is a type () of propositions, and there may be a type