Last modified on 12 June 2013, at 23:33

praeclarum theorema



So named by G.W. Leibniz in his unpublished papers of 1690 (later published as Leibniz: Logical Papers in 1966), meaning "splendid theorem" in Latin.


praeclarum theorema

  1. (logic) The following theorem of propositional calculus: (A → B) ∧ (C → D) → (A ∧ C → B ∧ D). [1] [2] [3] [4]
    What is now called the praeclarum theorema is actually "one half" of Leibniz's original theorem, which was like so: if A = B and C = D, then AC = BD, whose appearance is splendidly algebraic. (It can also be stated as (A ↔ B) ∧ (C ↔ D) → (A ∧ C ↔ B ∧ D).)
    The praeclarum theorema can be seen to correspond with the logical rule \wedge R of sequent calculus; given two sequents  A \vdash B and C \vdash D one may infer (through the sequent calculus) that  A, C \vdash B \wedge D, where the comma on the left side of the turnstile can be interpreted as a kind of conjunction. So perhaps the \wedge R rule, together with the I rule:  A \vdash A , and the disjunctive analogue \vee L, can help to interpret the sequent calculus as being rather "algebraic" (esp. if the syntactic consequence (represented by the turnstile) is compared to a preorder).

See alsoEdit


  1. ^
  2. ^
  3. ^ (Proposition 10)
  4. ^ Theorem prth698 at Metamath Proof Explorer