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]
    The praeclarum theorema can be seen to correspond with the rule R \otimes of linear logic; given two sequents  A \vdash B and C \vdash D one may infer (through the said rule) that  A, C \vdash B \otimes D. Then one may further infer, through the rule L\otimes, that A \otimes C \vdash B \otimes D.

See alsoEdit


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