4th axiom in his 1903 and then as his first "primitive proposition" of PM: "❋1.1 Anything implied by a true elementary proposition is true". Now he repeats it in his 1912 in a refined form: "Thus our principle states that if this implies that, and this is true, then that is true. In other words, 'anything implied by a true proposition is true', or 'whatever follows from a true proposition is true'. This principle he places great stress upon, stating that "this principle is really involved – at least, concrete instances of it are involved – in all demonstrations". He does not call his inference principle modus ponens, but his formal, symbolic expression of it in PM (2nd edition 1927) is that of modus ponens; modern logic calls this a "rule" as opposed to a "law". In the quotation that follows, the symbol "⊦" is the "assertion-sign" (cf PM:92); "⊦" means "it is true that", therefore "⊦p" where "p" is "the sun is rising" means "it is true that the sun is rising", alternately "The statement 'The sun is rising' is true". The "implication" symbol "⊃" is commonly read "if p then q", or "p implies q" (cf PM:7). Embedded in this notion of "implication" are two "primitive ideas", "the Contradictory Function" (symbolized by NOT, "~") and "the Logical Sum or Disjunction" (symbolized by OR, "⋁"); these appear as "primitive propositions" ❋1.7 and ❋1.71 in PM (PM:97). With these two "primitive propositions" Russell defines "p ⊃ q" to have the formal logical equivalence "NOT-p OR q" symbolized by "~p ⋁ q": "Inference. The process of inference is as follows: a proposition "p" is asserted, and a proposition "p implies q" is asserted, and then as a sequel the proposition "q" is asserted. The trust in inference is the belief that if the two former assertions are not in error, the final assertion is not in error. Accordingly, whenever, in symbols, where p and q have of course special determination " "⊦p" and "⊦(p ⊃ q)" " have occurred, then "⊦q" will occur if it is desired to put it on record. The process of the inference cannot be reduced to symbols. Its sole record is the occurrence of "⊦q". ... An inference is the dropping of a true premiss; it is the dissolution of an implication". In other words, in a long "string" of inferences, after each inference we can