[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [Samples] / syllogisms
Wed Nov 14 16:13:08 PST 2012

# 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.

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 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 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 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 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 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 if you can fill this hole]

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

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

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

44. |- (ui): Universal Instantiation
45. 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>>