[CG] Praeclarum Theorema

Praeclarum Theorema • 1 • https://inquiryintoinquiry.com/2023/10/13/praeclarum-theorema-1/ The praeclarum theorema, or splendid theorem, is a theorem of propositional calculus noted and named by G.W. Leibniz, who stated and proved it in the following manner. If a is b and d is c, then ad will be bc. This is a fine theorem, which is proved in this way: a is b, therefore ad is bd (by what precedes), d is c, therefore bd is bc (again by what precedes), ad is bd, and bd is bc, therefore ad is bc. Q.E.D. — Leibniz • Logical Papers, p. 41. Expressed in contemporary logical notation, the theorem may be written as follows. • ((a ⇒ b) ∧ (d ⇒ c)) ⇒ ((a ∧ d) ⇒ (b ∧ c)) Expressed as a logical graph under the existential interpretation, the theorem takes the shape of the following formal equivalence or propositional equation. Praeclarum Theorema • https://inquiryintoinquiry.files.wordpress.com/2020/09/praeclarum-theorema-… Reference — Leibniz, Gottfried W. (1679–1686?), “Addenda to the Specimen of the Universal Calculus”, pp. 40–46 in G.H.R. Parkinson (ed., trans., 1966), Leibniz : Logical Papers, Oxford University Press, London, UK. Readings — Jon Awbrey • Propositional Equation Reasoning Systems • https://oeis.org/wiki/Propositional_Equation_Reasoning_Systems John F. Sowa • Peirce's Rules of Inference • https://www.jfsowa.com/peirce/infrules.htm Resources — Logical Graphs • https://oeis.org/wiki/Logical_Graphs Logical Graphs • First Impressions • https://inquiryintoinquiry.com/2023/08/24/logical-graphs-first-impressions/ Logical Graphs • Formal Development • https://inquiryintoinquiry.com/2023/09/01/logical-graphs-formal-development… Metamath Proof Explorer • Praeclarum Theorema • https://us.metamath.org/mpegif/mmset.html • https://us.metamath.org/mpegif/prth.html Frithjof Dau • Animated Proof of Leibniz's Praeclarum Theorema • http://dr-dau.net/ • http://dr-dau.net/pc.shtml Regards, Jon