Praeclarum Theorema

[Jon Awbrey]

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-3.0.png

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-a/

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

#Peirce #Logic #LogicalGraphs #EntitativeGraphs #ExistentialGraphs
#SpencerBrown #LawsOfForm #BooleanFunctions #PropositionalCalculus

[Jon Awbrey]

Praeclarum Theorema • 1
• https://inquiryintoinquiry.com/2023/10/13/praeclarum-theorema-1/

[Note. Fixing Formatting and Adding Figure]

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-3.0.png

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-a/

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

[Jon Awbrey]

Praeclarum Theorema • 2
• https://inquiryintoinquiry.com/2023/10/14/praeclarum-theorema-2/

Re: Praeclarum Theorema • 1
• https://inquiryintoinquiry.com/2023/10/13/praeclarum-theorema-1/

All,

Here's a neat proof of that nice theorem —

Praeclarum Theorema • Proof
• https://inquiryintoinquiry.files.wordpress.com/2020/09/praeclarum-theorema-e280a2-proof-3.0.png

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-a/

Metamath Proof Explorer • Praeclarum Theorema

• https://us.metamath.org/mpeuni/mmset.html
• https://us.metamath.org/mpeuni/prth.html

Frithjof Dau • Animated Proof of Leibniz's Praeclarum Theorema
• http://dr-dau.net/
• http://dr-dau.net/pc.shtml

Regards,

Jon

cc: https://www.academia.edu/community/LEBMYl

[Jon Awbrey]

Praeclarum Theorema • 3
• https://inquiryintoinquiry.com/2023/10/15/praeclarum-theorema-3/

Re: Praeclarum Theorema
• https://inquiryintoinquiry.com/2023/10/13/praeclarum-theorema-1/
• https://inquiryintoinquiry.com/2023/10/14/praeclarum-theorema-2/

The steps of the proof are replayed in the following animation.

Praeclarum Theorema • Proof Animation
• https://inquiryintoinquiry.files.wordpress.com/2012/01/praeclarum-theorema-2-0-animation.gif

Regards,

Jon

cc: https://www.academia.edu/community/LgwneL