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.
 To demonstrate that the logic developed in
[ ../maths/ ]
is at least as powerful as that taught 1000 years
ago.
 Explore the differences between ancient and modern logic.
 Provide a collection of examples of proofs.
 To provide a collection readtouse theorems.
 To improve the MATHS system of reasoning by using it.
. . . . . . . . . ( end of section Purposes of this page) <<Contents  End>>
 A syllogism is any argument that starts with two premises/givens and deduces a single conclusion from them.
 The most famous ones are the
Categorical Syllogisms
described on this page.
 I started with the list on Tom Van Vleck's web site.
[ petrushispanius.html ]
 A categorical syllogism is always about the properties of objects in a Universe of Discourse.
 U::Types=The Universe of Discourse.
 In Categorical Syllogisms the properties are expressed as predicates.
 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.
 S, M, P:@U, predicates on universe U.
 I'm going to use Q as another predicate below:
 Q:@U.
 Each premise and conclusion has one of four forms:
TableMnemonic  English  Translations


A  All P is Q  P==>Q, no(P&~Q)

E  No P is Q  P==>~Q, no(P&Q)

I  Some P is Q  some(P&Q)

O  Some P is not Q  some(P&~Q)

(Close Table)
 These are easily expressed in modern set theory.
 The Notation P==>Q is short for for all x, if P(x) then Q(x).
 (ui, mp) (uimp): if P(x) and P==>Q then Q(x).
 We can prove P==>Q by assuming P(x) for some local variable x and proving Q(x).
 The notation ~P is the predicate negation, (~P)(x) = not P(x).
 The notation P&Q is the conjunction of two predicates: (P&Q)(x) = P(x) and Q(x).
 The expression "some(P)" is short for for some x(P(x))
 From some(P) we can deduce P(x) where x is a free (local and unused) variable.
 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(M,S,P)::=if (M==>P) and (S==>M) then (S==>P).
Let
 (let) (01): M==>P.
 (let) (02): S==>M.
 (01, 02) (03): S==>P.
(goal): S==>P.
Let x, S(x).
 (let, 02, uimp)M(x),
 (01, uimp)P(x).
(Close Let )
 (above)for all x, if S(x) then P(x),
 (def)S==>P.
(Close Let )
 celarent(S,M,P)::=if no(M&P) and S==>M then no(S&P).
 (above)celarent(S,M,P).
Let
 (11): no(M&P).
 (let) (12): S==>M.
 (let) (13): not no(S&P).
 (13, def(no), dn) (14): for some x(S(x) and P(x)).
 (14, ei, x=>x)(15) S(x) and P(x).
 (15, and1) (16): S(x).
 (15, and2) (17): P(x).
 (16, 12) (17): M(x).
 (11, def(no), ui, demorgan1) (18): not M(x) or not P(x).
 (18, 7, or1) (19): not P(x).
 (17, 19)false.
(Close Let )
A different formalism of celarent leads to a shorter proof:
 celarent2(S,M,P)::=if M==>~P and S==>M then S==>~P.
 (above)celarent2(S,M,P)=barbara(S, M, ~P).
 darii(S,M,P)::=if M==>P and some(S&M) then some(S&P).
 (above)darii(S,M,P).
Let
 (let) (21): M==>P.
 (let)some(S&M),
 (def, ei) (22): S(x) and M(x),
 (and2) (23): M(x),
 (uimp) (24): P(x).
 (22, and1)S(x),
 (and, 24)S(x) and P(x),
 (eg)for some x(S(x) and G(x)),
 (def)some(S&P).
(Close Let )
(ferioque): Ferio is also known as Ferioque.
 ferio(S,M,P)::=if no(M&P) and some(S&M) then some(S&~P).
 (above)ferio(S,M,P).
Let
 (let) (31): no(M&P).
 (let)some(S&M),
 (def, ei) (32): S(x) and M(x).
 (32, and1) (33): S(x).
 (32, and2) (34): M(x).
 (31, def, ui, demorgan1) (35): not M(x) or not P(x),
 (34, or1)not P(x),
 (32, and) (36): S(x) and not P(x),
 (eg, def)some(S&~P).
(Close Let )
The C and the S in the mnemonic "CeSare" indicates that a Simple conversion
makes Cesare into Celarent.
 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.
 (above)cesare(S,M,P).
Let
 (let) (hyp40): P==>~M and S==>M.
Let x, S(x),
 (hyp40, and2, uimp) (41): M(x).
Let P(x),
 (hyp40, and1, def, ui)if P(x) then not M(x),
 (mp)not M(x),
 (41)false.
(Close Let )
 (RAA)not P(x)
(Close Let )
 (above)for all x, if S(x) then not P(x),
 (def)S==> ~P.
(Close Let )
The C and M in this mnemonic indicates that CameStres can be
converted (simply) to Celarent.
 camestres(S,M,P)::=if P==>M and no(S & M) then no(S&P).
Here is a natural deduction proof:
 (above)camestres(S,M,P)
Let
 (let) (hyp50): P==>M and no(S & M),
 (let)not no(S&P),
 (dn)some(S&P),
 (ei) (51): S(x) and P(x),
 (and2) (52): P(x),
 (hyp50, and1, uimp) (53): M(x).
 (51, and1)S(x),
 (and2)S(x) and M(x),
 (eg) (54): some(S&M),
 (hyp50, and2)no(S&M),
 (54)false.
(Close Let )
 (RAA)camestres(S,M,P).
 festino(S,M,P)::=if no(P&M) and some(S&M) then some(S&~P).
 (above)festino(S,M,P)
Let
 (let) (60): no(P&M).
 (let) (61): some(S&M).
 (61) (63): S(x) and M(x),
 (and1) (64): S(x).
 (61, and2) (65): M(x).
 (60, ui, mtp)not P(x),
 (eg)some(S&~P).
(Close Let )
(fakofo): Baroko is also known as Fakofo.
 baroko(S,M,P)::=if P==>M and some(S&~M) then some(S&~P).
Here is an abbreviated proof.
 (above)baroko(S,M,P).
Let
 (let) (66): P==>M.
 (let)some(S&~M),
 (def, ei, def) (67): S(x) and not M(x).
 (67, and2)not M(x),
 (66, ui, mtp) (68): not P(x).
 (67, and1, 68, and3, eg, def)some(S&~P).
(Close Let )
 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.
 (above)darapti(S,M,P).
Let
 (let) (70): M==>P.
 (let) (71): M==>S.
 (let)some M,
 (ei)M(x),
 (70, uimp) (72): P(x).
 (71, uimp)S(x),
 (72, and3)S(x) and P(x),
 (eg, def)some(S&P).
(Close Let )
 disamis(S,M,P)::= if some(M&P) and M==>S then some(S&P).
 (above)disamis(S,M,P).
Let
 (let)some(M&P),
 (def, ei) (75): M(x) & P(x).
 (let)M==>S,
 (and1, 75, uimp) (76): S(x),
 (75, and2, and)S(x) and P(x),
 (eg)some(S&P).
(Close Let )
 datisi(S,M,P)::=if M==>P and some(M&S) then some(S&P).
 (above)datisi(S,M,P).
Let
 (let) (80): M==>P.
 (let)some(M&S),
 (def, ei) (81): M(x) and S(x),
 (and1, uimp) (82): P(x).
 (81, and2, 82, and3, and5, eg)some(S&P).
(Close Let )
 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.
 (above)felapton(S,M,P).
Let
 (let) (85): M ==> ~P.
 (let) (84): M==>S.
 (let)some(M),
 (def, ei) (86): M(x),
 (84, uimp) (87): S(x).
 (85, uimp)not P(x),
 (87, and3, eg)some(S&~P).
(Close Let )
(dokamok): This is also called Dokamok.
 bocardo(S,M,P)::=if some(M&~P) and M==>S then some(S&~P).
 (above)bocardo(S,M,P).
Let
 (let)some(M&~P),
[click here if you can fill this hole]
 (above) (90): M(x) and not P(x),
 (and1) (91): M(x).
 (90, and2) (93): not P(x).
 (91, let)M==>S,
 (uimp)S(x),
 (93, and3, eg, def, def)some(S&~P).
(Close Let )
 ferison(S,M,P)::=if M==>~P and some(M&S) then some(S&~P).
 (above)ferison(S,M,P).
Let
 (let) (95): M==>~P.
 (let)some(M&S),
 (def, ei) (96): M(x) and S(x),
 (95, uimp, def) (97): not P(x).
 (96, and2)S(x),
 (97, and3)S(x) amd mot P(x),
 (def, def)some(S&~P).
(Close Let )
 bramantip(S,M,P)::=if P==>M and M==>S and some P then some S is P.
Let
 (let) (100): P==>M.
 (let) (101): M==>S.
 (let) (102): some P.
[click here if you can fill this hole]
(Close Let )
 camenes(S,M,P)::=if P==>M and no(M & S) then no(S&P).
[click here if you can fill this hole]
 dimaris(S,M,P)::=if some(P&M) and M==>S then some (S&P).
[click here if you can fill this hole]
 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(S,M,P)::=if no(P&M) and some(M&S) then some(S&~P).
[click here if you can fill this hole]
 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:
  (and1): If P and Q then P.
  (and2): If P and Q then Q.
  (demorgan1): not(P and Q) iff not P or not Q.
  (and3): If P and Q then (P and Q),  combines two proven results into one.
  (and4): P and P iff P, idempotent.
  (and5): P and Q iff Q and P, commutative.
  (and6): (P and Q) and R iff P and (Q and R), associative`.
  (or1): If (P or Q) and not P then Q, modus tolens.
  (or2): If (P or Q and not Q then P, modus tolens.
  (or3): P or P iff P, idempotent.
  (or4): (P or Q) iff (Q or P), commutative.
  (or5): (P or Q) or R iff P or (Q or R), associative.
  (demorgan2): not(P or Q) iff not P and not Q.
  (nor1): If not(P or Q) then not P.
  (nor2): If not(P or Q) then not Q.
 (above) (dn): not not P iff P.
  (dist1): P and (Q or R) iff (P and Q) or (P and R).
  (dist2): P or (Q and R) iff (P or Q) and (P or R).
  (abs1): P and(P or Q) iff (P or Q).
  (abs2): P or (P and Q) iff (P and Q).
  (mp): If (P and(if P then Q)) then Q, modus ponens.
  (mtp): If (not Q) and (if P then Q) then not P, modus tolendo ponens.
 (above) (iftrans): If (if P then Q) and (if Q then R) then (if P then R).
  (nif1): If not(if P then Q) then P.
  (nif2): If not(if P then Q) then not Q.
  (nif3): If not(if P then Q) then P and not Q.
 (nif1,nif2,nif3) (nif4): not(if P then Q) iff P and not Q.
  (iff1): If (P iff Q) then (if P then Q).
  (iff2): If (P iff Q) then (if Q then P).
  (iff3): If ((if Q then P) and (if Q then P)) then (P iff Q)
  (iff4): (P iff Q) iff ( ((Q and P) or (not P and not Q))).
 (iff4) (iff5): (P iff Q)iff(Q iff P), commutative.
 (above) (iff6): (P iff (Q iff R) iff ((P iff Q) iff R), associative.
 (above) (ifftrans): If (P iff Q) and (Q iff R) then (P iff R).
  (niff): If not (P iff Q) then ((Q and not P) or (not P and Q)).
  (qn1): not for some x:T(W(x)) iff for all x:T(not W(x)).
  (qn2): not for all x:T(W(x)) iff for some x:T(not W(x)).
Table
(label) Name  From  Step  Conclude  When


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

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

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

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

(Close Table)
This is a useful lemma that follows from
ui and mp above.
 (ui, mp)if P(x) and P==>Q then Q(x).
Let
 (uimp1): P(x).
 (uimp2): P==>Q.
 (uimp2) (uimp3): for all x, if P(x) then Q(x).
 (uimp3, ui) (uimp4): if P(x) then Q(x).
 (uimp4, mp)Q(x).
(Close Let )
 let::=indicates a hypothesis introduced locally to prove a different result.
 def::=indicates the use of a definition.