PM ✱4·11 (Transp): $(p \equiv q) \equiv ({\sim} p \equiv {\sim} 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·11 (Transp): Whitehead and Russell, Principia Mathematica, Vol. I (1910), Part I, Section A, p. 122. 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.

PM refers to this proposition by the name Transp (Vol. I, Alphabetical list of propositions referred to by names), and cites it by that name in later proofs.

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_11 of the bundle PM_core_statement_formulas. Brackets are written out in full here in place of PM's dots.

Lean/Mathlib counterpart: not_iff_not (Mathlib at 0df444a; its proof is classical; with the two sides of an equivalence the other way round). It states the same law for Lean's own propositions, connective for connective.

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