[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [Samples] / syllogisms
[Index] [Contents] [Source Text] [About] [Notation] [Copyright] [Comment/Contact] [Search ]
Wed Nov 14 16:13:08 PST 2012

Contents

    Medieval Categorical Syllogisms

      Status

      I started this page on July 26th 2005 and I developed it alone until August 29th 2005. From now on changes will occur when people "fill in the Holes" below or point out errors.

      If you want to have a go, select the "Contact" link above, or find a "Hole"/"plugin" link and EMail me your ideas using the form that pops up. I will edit(if necessary), publish, and give you credit.

      Purposes of this page

      1. To demonstrate that the logic developed in [ ../maths/ ] is at least as powerful as that taught 1000 years ago.
      2. Explore the differences between ancient and modern logic.
      3. Provide a collection of examples of proofs.
      4. To provide a collection read-to-use theorems.
      5. To improve the MATHS system of reasoning by using it.

      . . . . . . . . . ( end of section Purposes of this page) <<Contents | End>>

      Notes

    1. A syllogism is any argument that starts with two premises/givens and deduces a single conclusion from them.
    2. The most famous ones are the Categorical Syllogisms described on this page.
    3. I started with the list on Tom Van Vleck's web site. [ petrus-hispanius.html ]
    4. A categorical syllogism is always about the properties of objects in a Universe of Discourse.
    5. U::Types=The Universe of Discourse.
    6. In Categorical Syllogisms the properties are expressed as predicates.
    7. The premisses and conclusion are formulae that contain 3 predicates symbolized: S, M, and P. All the formula have a form with two of these.
    8. S, M, P:@U, predicates on universe U.
    9. I'm going to use Q as another predicate below:
    10. Q:@U.
    11. Each premise and conclusion has one of four forms:
      Table
      MnemonicEnglishTranslations
      AAll P is QP==>Q, no(P&~Q)
      ENo P is QP==>~Q, no(P&Q)
      ISome P is Qsome(P&Q)
      OSome P is not Qsome(P&~Q)

      (Close Table)
    12. These are easily expressed in modern set theory.
    13. The Notation P==>Q is short for for all x, if P(x) then Q(x).
    14. (ui, mp)|- (uimp): if P(x) and P==>Q then Q(x).
    15. We can prove P==>Q by assuming P(x) for some local variable x and proving Q(x).
    16. The notation ~P is the predicate negation, (~P)(x) = not P(x).
    17. The notation P&Q is the conjunction of two predicates: (P&Q)(x) = P(x) and Q(x).
    18. The expression "some(P)" is short for for some x(P(x))
    19. From some(P) we can deduce P(x) where x is a free (local and unused) variable.
    20. The expression "no(P)" is short for for no x(P(x)) and is equivalent to not some(P) and for all x(not P(x)).

      Barbara : If all M is P and all S is M then all S is P

    21. barbara(M,S,P)::=if (M==>P) and (S==>M) then (S==>P).
      Let

      1. (let)|- (01): M==>P.
      2. (let)|- (02): S==>M.
      3. (01, 02)|- (03): S==>P.

        Proof of 03


        (goal): S==>P.
        Let
        1. x, S(x).
        2. (let, 02, uimp)|-M(x),
        3. (01, uimp)|-P(x).

        (Close Let )

      4. (above)|-for all x, if S(x) then P(x),
      5. (def)|-S==>P.


      (Close Let )

      Celarent : If no M is P and all S is M then no S is P

    22. celarent(S,M,P)::=if no(M&P) and S==>M then no(S&P).
    23. (above)|-celarent(S,M,P).
      Let
      1. (11): no(M&P).
      2. (let)|- (12): S==>M.
      3. (let)|- (13): not no(S&P).
      4. (13, def(no), dn)|- (14): for some x(S(x) and P(x)).
      5. (14, ei, x=>x)|-(15) S(x) and P(x).
      6. (15, and1)|- (16): S(x).
      7. (15, and2)|- (17): P(x).
      8. (16, 12)|- (17): M(x).
      9. (11, def(no), ui, demorgan1)|- (18): not M(x) or not P(x).
      10. (18, 7, or1)|- (19): not P(x).
      11. (17, 19)|-false.

      (Close Let )

      A different formalism of celarent leads to a shorter proof:

    24. celarent2(S,M,P)::=if M==>~P and S==>M then S==>~P.
    25. (above)|-celarent2(S,M,P)=barbara(S, M, ~P).

      Darii : If all M is P and some S is M then some S is P

    26. darii(S,M,P)::=if M==>P and some(S&M) then some(S&P).
    27. (above)|-darii(S,M,P).
      Let

      1. (let)|- (21): M==>P.
      2. (let)|-some(S&M),
      3. (def, ei)|- (22): S(x) and M(x),
      4. (and2)|- (23): M(x),
      5. (uimp)|- (24): P(x).


      6. (22, and1)|-S(x),
      7. (and, 24)|-S(x) and P(x),
      8. (eg)|-for some x(S(x) and G(x)),
      9. (def)|-some(S&P).

      (Close Let )

      Ferio : If no M is P and some S is M then some S is not P


      (ferioque): Ferio is also known as Ferioque.

    28. ferio(S,M,P)::=if no(M&P) and some(S&M) then some(S&~P).
    29. (above)|-ferio(S,M,P).
      Let

      1. (let)|- (31): no(M&P).
      2. (let)|-some(S&M),
      3. (def, ei)|- (32): S(x) and M(x).
      4. (32, and1)|- (33): S(x).
      5. (32, and2)|- (34): M(x).
      6. (31, def, ui, demorgan1)|- (35): not M(x) or not P(x),
      7. (34, or1)|-not P(x),
      8. (32, and)|- (36): S(x) and not P(x),
      9. (eg, def)|-some(S&~P).

      (Close Let )

      Cesare : If no P is M and all S is M then no S is P

      The C and the S in the mnemonic "CeSare" indicates that a Simple conversion makes Cesare into Celarent.
    30. cesare(S,M,P)::=if P==>~M and S==>M then S==>~P.

      The simple conversion is to substitute (M==>~P) for the equivalent (P==>~M).

      Here is a draft proof, without the conversion, with some links and steps left out.

    31. (above)|-cesare(S,M,P).
      Let

      1. (let)|- (hyp40): P==>~M and S==>M.
        Let
        1. x, S(x),
        2. (hyp40, and2, uimp)|- (41): M(x).
          Let
          1. P(x),
          2. (hyp40, and1, def, ui)|-if P(x) then not M(x),
          3. (mp)|-not M(x),
          4. (41)|-false.

          (Close Let )

        3. (RAA)|-not P(x)

        (Close Let )

      2. (above)|-for all x, if S(x) then not P(x),
      3. (def)|-S==> ~P.

      (Close Let )

      Camestres : If all P is M and no S is M then no S is P

      The C and M in this mnemonic indicates that CameStres can be converted (simply) to Celarent.
    32. camestres(S,M,P)::=if P==>M and no(S & M) then no(S&P).

      Here is a natural deduction proof:

    33. (above)|-camestres(S,M,P)
      Let

      1. (let)|- (hyp50): P==>M and no(S & M),
      2. (let)|-not no(S&P),
      3. (dn)|-some(S&P),
      4. (ei)|- (51): S(x) and P(x),
      5. (and2)|- (52): P(x),
      6. (hyp50, and1, uimp)|- (53): M(x).
      7. (51, and1)|-S(x),
      8. (and2)|-S(x) and M(x),
      9. (eg)|- (54): some(S&M),
      10. (hyp50, and2)|-no(S&M),
      11. (54)|-false.

      (Close Let )

    34. (RAA)|-camestres(S,M,P).

      Festino : If no P is M and some S is M then some S is not P

    35. festino(S,M,P)::=if no(P&M) and some(S&M) then some(S&~P).
    36. (above)|-festino(S,M,P)
      Let

      1. (let)|- (60): no(P&M).
      2. (let)|- (61): some(S&M).
      3. (61)|- (63): S(x) and M(x),
      4. (and1)|- (64): S(x).
      5. (61, and2)|- (65): M(x).
      6. (60, ui, mtp)|-not P(x),
      7. (eg)|-some(S&~P).

      (Close Let )

      Baroko : If all P is M and some S is not M then some S is not P


      (fakofo): Baroko is also known as Fakofo.

    37. baroko(S,M,P)::=if P==>M and some(S&~M) then some(S&~P).

      Here is an abbreviated proof.

    38. (above)|-baroko(S,M,P).
      Let

      1. (let)|- (66): P==>M.
      2. (let)|-some(S&~M),
      3. (def, ei, def)|- (67): S(x) and not M(x).


      4. (67, and2)|-not M(x),
      5. (66, ui, mtp)|- (68): not P(x).
      6. (67, and1, 68, and3, eg, def)|-some(S&~P).

      (Close Let )

      Darapti : If all M is P and all M is S then some S is P

    39. darapti(S,M,P)::= if M==>P and M==>S and some M then some(S&P).

      Note. The ancients interpretted "All A is B" to imply "some A", But the moderns (after the late 1800s) started to drop this interpretation. In MATHS A==> B does not suggest (some A). So, to sve the argument an extra premise is needed.

    40. (above)|-darapti(S,M,P).
      Let

      1. (let)|- (70): M==>P.
      2. (let)|- (71): M==>S.
      3. (let)|-some M,
      4. (ei)|-M(x),
      5. (70, uimp)|- (72): P(x).
      6. (71, uimp)|-S(x),
      7. (72, and3)|-S(x) and P(x),
      8. (eg, def)|-some(S&P).

      (Close Let )

      Disamis : If some M is P and all M is S then some S is P

    41. disamis(S,M,P)::= if some(M&P) and M==>S then some(S&P).
    42. (above)|-disamis(S,M,P).
      Let

      1. (let)|-some(M&P),
      2. (def, ei)|- (75): M(x) & P(x).
      3. (let)|-M==>S,
      4. (and1, 75, uimp)|- (76): S(x),
      5. (75, and2, and)|-S(x) and P(x),
      6. (eg)|-some(S&P).

      (Close Let )

      Datisi : If all M is P and some M is S then some S is P

    43. datisi(S,M,P)::=if M==>P and some(M&S) then some(S&P).
    44. (above)|-datisi(S,M,P).
      Let

      1. (let)|- (80): M==>P.
      2. (let)|-some(M&S),
      3. (def, ei)|- (81): M(x) and S(x),
      4. (and1, uimp)|- (82): P(x).
      5. (81, and2, 82, and3, and5, eg)|-some(S&P).

      (Close Let )

      Felapton : If no M is P and all M is S then some S is not P

    45. felapton(S,M,P)::=if M==> ~P and M==>S and some(M) then some(S&~P). Felapton is only a valid inferrence in the modern sense when all M is S entail some M exists.
    46. (above)|-felapton(S,M,P).
      Let

      1. (let)|- (85): M ==> ~P.
      2. (let)|- (84): M==>S.
      3. (let)|-some(M),
      4. (def, ei)|- (86): M(x),
      5. (84, uimp)|- (87): S(x).
      6. (85, uimp)|-not P(x),
      7. (87, and3, eg)|-some(S&~P).

      (Close Let )

      Bocardo : If some M is not P and all M is S then some S is not P


      (dokamok): This is also called Dokamok.
    47. bocardo(S,M,P)::=if some(M&~P) and M==>S then some(S&~P).
    48. (above)|-bocardo(S,M,P).
      Let

      1. (let)|-some(M&~P), [click here [socket symbol] if you can fill this hole]
      2. (above)|- (90): M(x) and not P(x),
      3. (and1)|- (91): M(x).
      4. (90, and2)|- (93): not P(x).
      5. (91, let)|-M==>S,
      6. (uimp)|-S(x),
      7. (93, and3, eg, def, def)|-some(S&~P).

      (Close Let )

      Ferison : If no M is P and some M is S then some S is not P

    49. ferison(S,M,P)::=if M==>~P and some(M&S) then some(S&~P).
    50. (above)|-ferison(S,M,P).
      Let

      1. (let)|- (95): M==>~P.
      2. (let)|-some(M&S),
      3. (def, ei)|- (96): M(x) and S(x),
      4. (95, uimp, def)|- (97): not P(x).
      5. (96, and2)|-S(x),
      6. (97, and3)|-S(x) amd mot P(x),
      7. (def, def)|-some(S&~P).

      (Close Let )

      Bramantip : If all P is M and all M is S then some S is P

    51. bramantip(S,M,P)::=if P==>M and M==>S and some P then some S is P.
      Let

      1. (let)|- (100): P==>M.
      2. (let)|- (101): M==>S.
      3. (let)|- (102): some P. [click here [socket symbol] if you can fill this hole]

      (Close Let )

      Camenes : If all P is M and no M is S then no S is P

    52. camenes(S,M,P)::=if P==>M and no(M & S) then no(S&P). [click here [socket symbol] if you can fill this hole]

      Dimaris : If some P is M and all M is S then some S is P

    53. dimaris(S,M,P)::=if some(P&M) and M==>S then some (S&P). [click here [socket symbol] if you can fill this hole]

      Fesapo : If no P is M and all M is S then some S is not P

    54. fesapo(S,M,P)::=if no(P&M) and M==>S some M then some(S&~P). [click here [socket symbol] if you can fill this hole]

      Fresison : If no P is M and some M is S then some S is not P

    55. fresison(S,M,P)::=if no(P&M) and some(M&S) then some(S&~P). [click here [socket symbol] if you can fill this hole]

      Links

    56. LOGIC::=following,
        [ ../maths/logic_history.html ] [ ../maths/logic_0_Intro.html ] [ ../maths/logic_10_PC_LPC.html ] [ ../maths/logic_11_Equality_etc.html ] [ ../maths/logic_25_Proofs.html ]

        The above links import the following derivation rules and theorems:


        1. |- (and1): If P and Q then P.
        2. |- (and2): If P and Q then Q.
        3. |- (demorgan1): not(P and Q) iff not P or not Q.
        4. |- (and3): If P and Q then (P and Q), -- combines two proven results into one.
        5. |- (and4): P and P iff P, idempotent.
        6. |- (and5): P and Q iff Q and P, commutative.
        7. |- (and6): (P and Q) and R iff P and (Q and R), associative`.


        8. |- (or1): If (P or Q) and not P then Q, modus tolens.
        9. |- (or2): If (P or Q and not Q then P, modus tolens.
        10. |- (or3): P or P iff P, idempotent.
        11. |- (or4): (P or Q) iff (Q or P), commutative.
        12. |- (or5): (P or Q) or R iff P or (Q or R), associative.
        13. |- (demorgan2): not(P or Q) iff not P and not Q.
        14. |- (nor1): If not(P or Q) then not P.
        15. |- (nor2): If not(P or Q) then not Q.


        16. (above)|- (dn): not not P iff P.


        17. |- (dist1): P and (Q or R) iff (P and Q) or (P and R).
        18. |- (dist2): P or (Q and R) iff (P or Q) and (P or R).


        19. |- (abs1): P and(P or Q) iff (P or Q).
        20. |- (abs2): P or (P and Q) iff (P and Q).


        21. |- (mp): If (P and(if P then Q)) then Q, modus ponens.
        22. |- (mtp): If (not Q) and (if P then Q) then not P, modus tolendo ponens.
        23. (above)|- (iftrans): If (if P then Q) and (if Q then R) then (if P then R).
        24. |- (nif1): If not(if P then Q) then P.
        25. |- (nif2): If not(if P then Q) then not Q.
        26. |- (nif3): If not(if P then Q) then P and not Q.
        27. |-(nif1,nif2,nif3)|- (nif4): not(if P then Q) iff P and not Q.


        28. |- (iff1): If (P iff Q) then (if P then Q).
        29. |- (iff2): If (P iff Q) then (if Q then P).
        30. |- (iff3): If ((if Q then P) and (if Q then P)) then (P iff Q)
        31. |- (iff4): (P iff Q) iff ( ((Q and P) or (not P and not Q))).
        32. (iff4)|- (iff5): (P iff Q)iff(Q iff P), commutative.
        33. (above)|- (iff6): (P iff (Q iff R) iff ((P iff Q) iff R), associative.
        34. (above)|- (ifftrans): If (P iff Q) and (Q iff R) then (P iff R).


        35. |- (niff): If not (P iff Q) then ((Q and not P) or (not P and Q)).


        36. |- (qn1): not for some x:T(W(x)) iff for all x:T(not W(x)).
        37. |- (qn2): not for all x:T(W(x)) iff for some x:T(not W(x)).


          Table
          (label) NameFromStepConcludeWhen

        38. |- (eg): Existential Generalization
          		39. W(e) (eg, x=>e)|- for some x:T(W(x)) e must be an expression of type T

        39. |- (ei): Existential Instantiation
          		40. for some x:T(W(x)) (ei, x=>v)|- v:T, W(v) v must be free variable before, and is now bound.

        40. |- (ud): Unique definition
          		41. for one x:T(W(x)) (ud, v=>x)|- W(v) v must be free variable before, and is now bound.

        41. |- (ui): Universal Instantiation
          		42. for all x:T(W(x)) (ui, x=>e)|- W(e) e is an expression of type T

          (Close Table)

        Proof of uimp

        This is a useful lemma that follows from ui and mp above.
      1. (ui, mp)|-if P(x) and P==>Q then Q(x).
        Let
        1. (uimp1): P(x).
        2. (uimp2): P==>Q.
        3. (uimp2)|- (uimp3): for all x, if P(x) then Q(x).
        4. (uimp3, ui)|- (uimp4): if P(x) then Q(x).
        5. (uimp4, mp)|-Q(x).

        (Close Let )


    57. let::=indicates a hypothesis introduced locally to prove a different result.
    58. def::=indicates the use of a definition.

    . . . . . . . . . ( end of section Medieval Categorical Syllogisms) <<Contents | End>>

End