.Open 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.
.Open Purposes of this page
 To demonstrate that the logic developed in
.See ../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 read-to-use theorems.
 To improve the MATHS system of reasoning by using it.
.Close Purposes of this page
. Notes
 A syllogism is any argument that starts with two premises/givens and deduces a single conclusion from them.
 The most famous ones are the
.Key Categorical Syllogisms
described on this page.
 I started with the list on Tom Van Vleck's web site.
.See http://www.multicians.org/thvv/petrus-hispanius.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:
.Table Mnemonic	English	Translations
.Row A	All P is Q	P==>Q, no(P&~Q)
.Row E	No P is Q	P==>~Q, no(P&Q)
.Row I	Some P is Q	some(P&Q)
.Row 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 : If all M is P and all S is M then all S is P
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.
. Proof of 03
(goal): S==>P.
.Let x, S(x).
	(let, 02, uimp)|-M(x),
	(01, uimp)|-P(x).
.Close.Let
	()|-for all x, if S(x) then P(x),
	(def)|-S==>P.

.Close.Let
. Celarent : If no M is P and all S is M then no S is P
celarent(S,M,P)::=if no(M&P) and S==>M then no(S&P).
()|- 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.
()|- celarent2(S,M,P)=barbara(S, M, ~P).

. Darii : If all M is P and some S is M then some S is P
darii(S,M,P)::=if M==>P and some(S&M) then some(S&P).
()|-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
. Ferio : If no M is P and some S is M then some S is not P
(ferioque): Ferio is also known as Ferioque.

ferio(S,M,P)::=if no(M&P) and some(S&M) then some(S&~P).
()|-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

. 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.
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.
()|-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
	()|-for all x, if S(x) then not P(x),
	(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.
camestres(S,M,P)::=if P==>M and no(S & M) then no(S&P).

Here is a natural deduction proof:
()|-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 : If no P is M and some S is M then some S is not P
festino(S,M,P)::=if no(P&M) and some(S&M) then some(S&~P).
()|-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
. 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.

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

Here is an abbreviated proof.
()|-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 : If all M is P and all M is S then some S is P
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.
()|-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 : If some M is P and all M is S then some S is P
disamis(S,M,P)::= if some(M&P) and M==>S then some(S&P).
()|-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 : If all M is P and some M is S then some S is P
datisi(S,M,P)::=if M==>P and some(M&S) then some(S&P).
()|-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 : If no M is P and all M is S then some S is not P
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`.
()|-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
. Bocardo : If some M is not P and all M is S then some S is not P
(dokamok): This is also called Dokamok.
bocardo(S,M,P)::=if some(M&~P) and M==>S then some(S&~P).
()|-bocardo(S,M,P).
.Let
	(let)|- some(M&~P),
.Hole
	()|-(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 : If no M is P and some M is S then some S is not P
ferison(S,M,P)::=if M==>~P and some(M&S) then some(S&~P).
()|-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 : If all P is M and all M is S then some S is P
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.
.Hole
.Close.Let
. Camenes : If all P is M and no M is S then no S is P
camenes(S,M,P)::=if P==>M and no(M & S) then no(S&P).
.Hole
. Dimaris : If some P is M and all M is S then some S is P
dimaris(S,M,P)::=if some(P&M) and M==>S then some (S&P).
.Hole
. Fesapo : If no P is M and all M is S then some S is not P
fesapo(S,M,P)::=if no(P&M) and M==>S some M then some(S&~P).
.Hole
. Fresison : If no P is M and some M is S then some S is not P
fresison(S,M,P)::=if no(P&M) and some(M&S) then some(S&~P).
.Hole

. Links
LOGIC::=following,
.List
.See ../maths/logic_history.html
.See ../maths/logic_0_Intro.html
.See ../maths/logic_10_PC_LPC.html
.See ../maths/logic_11_Equality_etc.html
.See ../maths/logic_2_Proofs.html

The above links import the following derivation rules and theorems:
.Box
	|- (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.

        ()|- (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`.
	()|-(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.
	()|- (iff6): (P iff (Q iff R) iff ((P iff Q) iff R), associative.
	()|-(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
.Row |- (eg): Existential Generalization
.Item W(e)
.Item (eg, x=>e)|-
.Item for some x:T(W(x))  
.Item `e` must be an expression of type `T`
.Row
|- (ei): Existential Instantiation
.Item for some x:T(W(x))
.Item (ei, x=>v)|-
.Item v:T, W(v) 
.Item `v` must be free variable before, and is now bound.
.Row
|- (ud): Unique definition
.Item for one x:T(W(x))
.Item (ud, v=>x)|-
.Item W(v)	
.Item `v` must be free variable before, and is now bound.
.Row
|- (ui): Universal Instantiation
.Item for all x:T(W(x))
.Item (ui, x=>e)|-
.Item W(e)
.Item `e` is an expression of type `T`
.Close.Table
.Close.Box

. Proof of uimp
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

.Close.List
let::=`indicates a hypothesis introduced locally to prove a different result`.
def::=`indicates the use of a definition`.
.Close Medieval Categorical Syllogisms