I sillogismi secondo Lukasiewicz

Usiamo la notazione polacca di Lukasiewicz.
C=  (–>)
K=  (&)
N=  (~)

A= Universale Affermativa
E= Universale Negativa
I= Particolare Affermativa
O= Particolare Negativa

Assioma

S1: Aaa
Ogni a è a
S2: Iaa
Qualche a è a
S3: CKAmbAamAabSe ogni m è b & ogni a è m, allora ogni a è b
S4: CKAmbImaIabSe ogni m è b & qualche m è a, allora qualche a è b

Definizioni

D1: Oab=NAabQualche a non è b = Non ogni a è b
D2: Eab= NIabNessuna a è b = Qualche a non è b

Postulati

T1: Cpp
p implica p
T2: CCpqCCqrCpr
Se p implica q, allora se q implica r, allora p implica r
T3: CCpqCNqNp
Se p implica q allora non q implica non p
T4: CCpNqCqNp
Se p implica non q, allora q implica non p
T5: CCNpqCNqp
Se non p implica q, allora non q implica p
T6: CCKpqrCpCqr
Se p & q implica r, allora se p allora q implica r
T7: CCKpqrCqCpr
Se p & q implica r, allora se q allora p implica r
T8: CCKpqrCKpNrNq
Se p & q implica r allora p & non r implica non q
T9: CCKpqrCKNrqNp
Se p & q implica r allora non r & q implica non p
T10: CCKpqrCCspCKsqr
Se p & q implica r allora se s implica p allora s & q implica r
T11: CCKpqrCCsqCKpsr
Se p & q implica r allora se s implica q allora p & s implica r
T12: CCKpqrCCrsCKqps
Se p & q implica r allora se r implica s allora q & p implica s

Teoremi

Leggi del Quadrato delle Oppisizoni

S5 COabNAab
1. Cpp [sub p/NAab in T1]
2. CNAabNAab
3. COabNAab [by D1 of antecedent in 2]
Q.E.D.

S6 CNAabOab
1.Cpp [sub p/NAab in T1]
2. CNAabNAab
3. CNAabOab [D1 of consequent in 2]
Q.E.D.

S7 CAabNOab
1. CCpNqCqNp [sub. p/Oab, q/Aab in T4]
2. CCOabNAabCAabNOab
3. CAabNoab [by (2)/(S5) & MP]
Q.E.D.

S8 CNOabAab
1. CCNpqCNqp [sub. p/Aab, q/Oab in T5]
2. CCNAabOabCNOabAab
3. CNOabAab [by (2)/(S6) & MP]
Q.E.D.

S9 CEabNIab
1. Cpp [sub. p/NIab in T1]
2. CNIabNIab
3. CEabNIab [by D2 of antecedent in 2]
Q.E.D.

S10 CNIabEab
1. Cpp [sub. p/NIab in T1]
2. CNIabNIab
3. CNIabEab [by D2 of consequent in 2]
Q.E.D.

S11 CIabNEab
1. CCpNqCqNp [sub. p/Eab, q/Iab, in T4]
2. CCEabNIabCIabNEab
3. CIabNEab [by (2)/(S9) & MP]
Q.E.D.

S12 CNEabIab
1. CCNpqCNqp [sub. p/Iab, q/Eab in T5]
2. CCNIabEabCNEabIab
3. CNEabIab [by (2)/(S10) & MP]
Q.E.D.

Leggi di Subordinazioni

S13 CAabIab
1. CCKpqrCqCpr [sub. p/Aab, q/Iaa, r/Iab in T7]
2. CCKAabIaaIabCIaaCAabIab
3. CKAmbImaIab [sub. m/a in S4]
4. CKAabIaaIab
5. CIaaCAabIab [by (2)/4) & MP]
6. CAabIab [by (5)/(S2) & MP]
Q.E.D.

S14 CNIabNAab
1. CCpqCNqNp [sub. p/Aab, q/Iab in T3]
2. CCAabIabCNIabNab
3. CNIabNAab [by (2)/(S13) & MP]
Q.E.D.

S15 CEabOab
1. CNIabNAab [reiteration of S14]
2. CEabNAab [by D2 of antecedent of 1]
3. CEabOab [by D1 of consequent of 2]
Q.E.D.

Leggi dei Contrari

S16 CNOabNEab
1. CCpqCNqNp [sub. p/Eab, q/Oab, in T3]
2. CCEabOabCNOabNEab
3. CNOabNEab [by (2)/(S15) & MP]
Q.E.D.

S17 CEabNAab
1. CNIabNAab [reiteration S14]
2. CEabNAab [D2 of antecedent (1)]
Q.E.D.

S18 CAabNEab
1. CCpNqCqNp [sub. p/Eab, q/Aab in Th 4]
2. CCEabNAabCAabNEab
3. CAabNEab [by (2)/(S17) & MP]
Q.E.D.

Leggi dei Subcontrari

S19 CNIabOab
1. CNIabNAab [reiteration S14]
2. CNIabOab [by (1) & D1 consequent]
Q.E.D.

S20 CNOabIab
1. CCNpqCNqp [sub. p/Iab, q/Oab, in Th 5]
2. CCNIabOabCNOabIab
3. CNOabIab [by (S19)/(2) & MP]
Q.E.D.

Leggi di Conversione

S21 CIabIba
1. CCKpqrCpCqr [sub p/Aaa, q/Iab, r/Iba in Th 6]
2. CCKAaaIabIbaCAaaCIabIba
3. CKAmbImaIab [sub m/a, b/a, a/b in (S4)]
4. CKAaaIabIba
5. CAaaCIabIba [(2)/(4) & MP]
6. CIabIba [(S1)/(5) & MP]
Q.E.D.

S22 CAabIba
1. CCpqCqrCpr [sub p/Aab, q/Iab, r/Iba in Th 2]
2. CCAabIabCIabIbaCAabIba
3. CIabIbaCAabIba [by (2)/(S3) & MP]
4. CAabIba [by (3)/(S21) & MP]
Q.E.D.

S23 CNIabNIba
1. CCpqCNqNp [sub p/Iba, q/Iab, r/Iab in Th 3]
2. CCIbaIabCNIabNIba
3. CIabIba [sub a/b, b/a in (S21)]
4. CIbaIab
5. CNIabNIba [by (4)/(2) & MP]
Q.E.D.

S24 CEabNIba
1. CNIabNIba [reiteration (S23)]
2. CEabNIba [D2 of antecedent (1)]
Q.E.D.

S25 CEabEba
1. CEabNIba [reiteration (S24)]
2. Eba=NIba [sub a/b, b/a in D2]
3. CEabEba [by (1)/(2) D2 consequent (1)]
Q.E.D.

SILLOGISMO - FIGURA 1

S26 CKAmbAamIab (Barbari)
1. CCKpqrCCsqCKpsr [sub p/Amb, q/Ima, r/Iab, s/Aam in Th 11]
2. CCKambImaIabCCAamImaCKAmbAamIab
3. CCAamImaCKAmbAamIab [by (2)/(S4) & MP]
4. CAamIma [sub b/m in (S22)]
5. CKAmbAamIab [by (3)/(4) & MP]
Q.E.D.

S27 CKAmbNIabNIma
1. CCKpqrCKpNrNq [sub p/Amb, q/Ima, r/Iab in Th 8]
2. CCKAmbImaIabCKAmbNIabNIma
3. CKAmbNIabNIma [by (2)/(S4) & MP]
Q.E.D.

S28 CKAmbEbaNIma
1. CCKpqrCCsqCKpsr [sub p/Amb, q/NIab, r/NIab, s/Eba in Th 11]
2. CCKAambNIabNImaCCEbaNIabCKAmbEbaNIma
3. CCEbaNIabCKAmbEbaNIam [by (2)/(S27) & MP]
4. CEabNIba [sub a/b, b/a in (S24)]
5. CEbaNIab
6. CKAmbEbaNIam [by (3)/(5) & MP]
Q.E.D

S29 CKEmbAamEab (Celarent)
1. CCKpqrCCrsCKqps [sub p/Aam, q/Emb, r/NIab, s/Eab in Th 12]
2. CCKAamEmbNIabCCNIabEabCKEmbAamEab
3. CKAmbEbaNIma [sub m/a, b/m, a/b in (S28)]
4. CKamEmbNIab
5. CCNIabEabCKEmbAamEab [by (3)/(4) & MP]
6. CKEmbAamEab [by (5)/(S10) & MP]
Q.E.D.

S30 CKEmbAamOab (Celaront)
1. CCpqCCqrCpr [sub p/KEmbAam, q/Eab, r/Oab in Th 2]
2. CCKEmbAamEabCCEabOabCKEmbAamOab
3. CCEabOabCKEmbAamOab [by (2)/(S29) & MP]
4. CKEmbAamOab [by (3)/(S15) & MP]
Q.E.D.

S31 CKEmbIamIab (Darii)
1. CCKpqrCCsqCKpsr [sub p/Amb, q/Ima, r/Iab, s/Iam in Th 11]
2. CCKAmbImaIabCCIamImaCKAmbIamIab
3. CCIamIMaCKAmbIamIab [by (2)/(S4) & MP]
4. CIabIba [reiteration (S21) & sub m/b]
5. CIamIma
6. CKAmbIamIab [by (3)/(5) & MP]
Q.E.D.

S32 CKNIabImaNAmb
1. CCKpqrCKNrqNp [sub p/Amb, q/Ima, r/Iab, in Th 9]
2. CCKAmbImaIabCKNIabImaNAmb
3. CKNIabImaNAmb pby (2)/(S4) & MP]
Q.E.D.

S33 CKEmbIamOab (Ferio)
1. CKNIabImaNAmb [sub a/m, m/a in (S32)]
2. CKNImbIamNAab
3. Emb=NImb [D2 sub a/m]
4. CKEmbIamNAab
5. CKEmbIam Oab [by (4) & D1 on consequent of (4)]
Q.E.D.

SILLOGISMO - FIGURA 2

S34 CKEbmAamEab (Cesare)
1. CCKpqrCCspCKsqr [sub p/Emb, q/Aam, r/Eab, s/Ebm in Th 10]
2. CCKEmbAamEabCCEbmEmbCKEbmAamEab
3. CCEbmEmbCKEbmAamEab [(2)/(S29) & MP]
4. CEabEba [sub a/b, b/m in (S24)]
5. CEbmEmb
6. CKEbmAamEab [by (5)/(3) & MP]
Q.E.D.

S35 CKEbmAamOab
1. CCpqCCqrCpr [sub p/KEbmAam, q/Eab, r/Oab in Th 2]
2. CCKEbmAamEabCCEabOabCKEbmAamOab
3. CCEabOabCKEbmAamOab [(2)/(S34) & MP]
4. CKEbmAamOab [by (3)/(S15) & MP]
Q.E.D.

S36 CKAbmEamEab (Camestres)
1. CCKpqrCCrsCKqps [sub p/Eam, q/Abm, r/Eba, S/Eab in Th 12]
2. CCKEamAbmEbaCCEbaEabCKAbmEamEab
3. CKEbmAamEab [sub b/a, a/b in (S34)]
4. CKEamAbmEba
5. CCEbaEabCKAbmEamEab [by (2)/(4) & MP]
6. CEabEba [sub a/b, b/a in (S25)]
7. CEbaEab
8. CKAbmEamEab [by (5)/(7) & MP]
Q.E.D.

S37 CKAbmEamOab (Camestrop)
1. CCpqCCqrCpr [sub p/KAbmEam, q/Eab, r/Oab in Th 2]
2. CCKAbmEamEabCCEabOabCKAbmEamOab
3. CCEabOabCKAbmEamOab [by (2)/(S36) & MP]
4. CKAbmEamOab [by (3)/(S15) & MP]
Q.E.D.

S38 CKEbmIamOab (Festino)
1. CCKpqrCCspCKsqr [sub p/Emb, q/Iam, r/Oab, s/Ebm in Th 10]
2. CCKEmbIamOabCCEbmEmbCKEbmIamOab
3. CCEbmEmbCKEbmIamOab [by (2)/(S33) & MP]
4. CEabEba [sub a/b, b/m by (S25)]
5. CEbmEmb
6. CKEbmIamOab [by (3)/(5) & MP]
Q.E.D.

S39 CKAmbNAabNAam
1. CKpqrCKpNrNq [sub p/Amb, q/Aam, r/Aab in Th 8]
2. CCKAmbAamAabCKAmbNAabNAam
3. CKAmbNAabNAam [by (2)/(S3) & MP]
Q.E.D.

S40 CKAbmOamOab (Baroco)
1. CKAmbNAabNAam [sub m/b, b/m in (S39)]
2. CKAbmNAamNAab
3. Oab=NAab [sub b/m in D1]
4. Oam=NAam
5. CKAbmOamOab [D1 of consequent (2)]
Q.E.D.

SILLOGISMO - FIGURA 3

S41 CKAmbAmaIab (Darapti)
1. CCKpqrCCsqCKpsr [sub p/Amb, q/Ima, r/Iab, s/Ama in Th 11]
2. CCKAmbImaIabCCAmaImaCKAmbAmaIab
3. CCAmaImaCKAmbAmaIab [by (2)/(S4) & MP]
4. CAabIab [sub a/m, b/a in (S13)]
5. CAmaIma
6. CKAmbAmaIab [by (5)/(3) & MP]
Q.E.D.

S42 CKEmbAmaOab (Felapton)
1. CCKpqrCCsqCKpsr [sub p/Emb, q/Iam, r/Oab, s/Ama in Th 11]
2. CCKEmbIamOabCCAmaIamCKEmbAmaOab
3. CCAmaIamCKEmbAmaOab [by (2)/(S33) & MP]
4. CAabIba [sub a/m, b/a in (S22)]
5. CAmaIam
6. CKEmbAmaOab [by (5)/(3) & MP]
Q.E.D.

S43 CKImbAmaIab (Disamis)
1. CCKpqrCCrsCKqps [sub p/Ama, q/Imb, r/Iba, s/Iab in Th 12]
2. CCKAmaImbIbaCCIbaIabCKImbAmaIab
3. CKAmbImaIab [sub b/a, a/b in (S4)]
4. CKAmaImbIba
5. CCIbaIabCKImbAmaIab [by (4)/(2) & MP]
6. CIabIba [sub a/b, b/a in (S21)]
7. CIbaIab
8. CKImbAmaIab [by (5)/(7) & MP]
Q.E.D.

S44 CKNAabAamNAmb
1. CCKpqrCKNrqNp [sub p/Amb, q/Aam, r/Aab in Th 9]
2. CCKAmbAamAabCKNAabAamNAmb
3. CKNAabAamNAmb [by (2)/(S3) & MP]
Q.E.D.

S45 CKOmbAmaOab (Bocardo)
1. CKNabAamNAmb [sub a/m, m/a in (S44)]
2. CKNAmbAmaNAab
3. Oab=NAab [sub a/m in D1]
4. Omb=NAmb
5. CKOmbAmaNAab
6. CKOmbAmaOab [by D1 of consequent in (5)]
Q.E.D.

S46 CKEmbImaOab (Fersion)
1. CCKpqrCCsqCKpsr [sub p/Emb, q/Iam, r/Oab, s/Ima in Th 11]
2. CCKEmbIamOabCCImaIamCKEmbImaOab
3. CCImaIamCKEmbImaOab [by (2)/(S33) & MP]
4. CIabIba [sub a/m, b/a in (S21)]
5. CImaIam
6. CKEmbImaOab [by (5)/(3) & MP]
Q.E.D.

SILLOGISMO - FIGURA 4

S47 CKAbmAmaIab (Bamalip)
1. CCKpqrCCspCKsqr [sub p/Imb, q/Ama, r/Iab, s/Abm in Th 10]
2. CCKImbAmaIabCCAbmImbCKAbmAmaIab
3. CCAbmImbCKAbmAmaIab [by (2)/(S43) & MP]
4.CAabIba [sub a/b, b/a in (S22)]
5. CAbmImb
6. CKAbmAmaIab [by (5)/(3) & MP]
Q.E.D.

S48 CKAbmEmaEab (Calemes)
1. CCKpqrCCsqCKpsr [sub p/Abm, q/Eam, r/Eab, s/Ema in Th 11]
2. CCKAbmEamEabCCEmaEamCKAbmEmaEab
3. CCEmaEamCKAbmEmaEab [by (2)/(S36) & MP]
4. CEabEba [sub a/m, b/a in (S25)]
5. CEmaEam
6. CKAbmEmaEab [by (5)/(3) & MP]
Q.E.D.

S49 CKAbmEmaOab (Calemop)
1. CCpqCCqrCpr [sub p/KAbmEma, q/Eab, r/Oab in Th 2]
2. CCKAbmEmaEabCCEabOabCKAbmEmaOab
3. CCEabOabCKAbmEmaOab [by (2)/(S48) & MP]
4. CKAbmEmaOab [by (3)/(S15) & MP]
Q.E.D.

S50 CKIbmAmaIab (Diamtis)
1. CCKpqrCCspCKsqr [sub p/Imb, q/Ama, r/Iab, s/Ibm in Th 10]
2. CCKImbAmaIabCCIbmImbCKIbmAmaIab
3. CCIbmImbCKIbmAmaIab [by (2)/(S43) & MP]
4. CIabIba [sub a/b, b/m in (S21)]
5. CIbmImb
6. CKIbmAmaIab [by (3)/(5) & MP]
Q.E.D.

S51 CKEbmAmaOab
1. CCKpqrCCspCKsqr [sub p/Emb,q/Ama, r/Oab, s/Ebm]
2. CCKEmbAmaOabCCEbmEmbCKEbmAmaOab
3. CCEbmEmaCKEbmAmaOab [by (2)/(S46) & MP]
4. CEabEba [sub a/b, b/m in (S25)]
5. CEbmEmb
6. CKEbmAmaOab [by (5)/(3) & MP]
Q.E.D.

S52 CKEbmImaOab (Fression)
1. CCKpqrCCspCKsqr [sub p/Emb, q/Ima, r/Oab, s/Ebm in Th 10]
2. CCKEmbImaOabCCEbmEmbCKEbmImaOab
3. CCEbmEmbCKEbmImaOab [by (2)/(S46) & MP]
4. CEabEba [sub a/b, b/m in (S25)]
5. CEbmEmb
6. CKEbmImaOab [by (5)/(3) & MP]
Q.E.D.