PM ✱4·7: $(p \supset q) \equiv (p \supset (p \land q))$

DRAFT — part of an in-progress public formalization of Principia Mathematica; it may still change, and every change is dated in the project's change log.

Principia Mathematica ✱4·7: Whitehead and Russell, Principia Mathematica, Vol. I (1910), Part I, Section A, p. 126. PM prints (Gutenberg #78050 transcription):

Formulas of PM's propositional calculus are built from propositional variables by negation ${\sim}$ and disjunction $\lor$, PM's two primitive ideas (✱1). Implication, conjunction and equivalence are PM's definitions: $p \supset q$ is ${\sim}p \lor q$ (✱1·01), $p \land q$ (PM writes $p\,.\,q$) is ${\sim}({\sim}p \lor {\sim}q)$ (✱3·01), and $p \equiv q$ is $(p \supset q) \land (q \supset p)$ (✱4·01). A theorem of ✱1 is a formula derivable from the primitive propositions ✱1·2–✱1·6 by the rule of inference ✱1·1 (from $p$ and $p \supset q$, infer $q$).

For all formulas $p$, $q$, the formula

is a theorem of ✱1.

It is one of the propositions of ✱4 from which PM builds the propositional calculus used throughout the work.

Formalization Note Deep embedding of PM ✱1: formulas are the inductive type PM.F (variables named by strings), the theorems of ✱1 are the inductive predicate PM.Thm, whose constructors are ✱1·1–✱1·6, and ✱1·01, ✱3·01, ✱4·01 are reducible definitions (F.imp, F.and, F.iff), so PM's definitions hold by definition. The statement formula is the definition PM.s4_7 of the bundle PM_core_statement_formulas. Brackets are written out in full here in place of PM's dots.

Source: PM.t4_7 in PM/Replay2.lean at commit 2e43991fec42.