CATEGORICAL SYLLOGISMS IN FIRST-ORDER LOGIC
===========================================
4 Examples from http://en.wikipedia.org/wiki/Syllogism#Barbara_.28AAA-1.29
Barbara (AAA-1)
***************
All men are mortal
All Greeks are men
---------------------
All Greeks are mortal
Major Premise:
1 ALL(a):[Man(a) => Mortal(a)]
Premise
Minor Premise:
2 ALL(a):[Greek(a) => Man(a)]
Premise
Suppose...
3 Greek(x)
Premise
Applying Minor Premise
4 Greek(x) => Man(x)
U Spec, 2
Applying Major premise
5 Man(x) => Mortal(x)
U Spec, 1
6 Man(x)
Detach, 4, 3
7 Mortal(x)
Detach, 5, 6
Conclusion:
8 ALL(a):[Greek(a) => Mortal(a)]
4 Conclusion, 3
Celarent (EAE-1)
****************
No reptiles have fur
All snakes are reptiles
-----------------------
No snakes have fur
Major Premise:
9 ALL(a):[Reptile(a) => ~Furry(a)]
Premise
Minor Premise:
10 ALL(a):[Snake(a) => Reptile(a)]
Premise
Suppose...
11 Snake(x)
Premise
Applying Minor Premise...
12 Snake(x) => Reptile(x)
U Spec, 10
Applying Major Premise...
13 Reptile(x) => ~Furry(x)
U Spec, 9
14 Reptile(x)
Detach, 12, 11
15 ~Furry(x)
Detach, 13, 14
Conclusion:
16 ALL(a):[Snake(a) => ~Furry(a)]
4 Conclusion, 11
Darii (AII-1)
*************
All rabbits have fur
Some pets are rabbits
---------------------
Some pets have fur
Major Premise:
17 ALL(a):[Rabbit(a) => Furry(a)]
Premise
Minor Premise:
18 EXIST(a):[Pet(a) & Rabbit(a)]
Premise
Applying Minor Premise...
19 Pet(x) & Rabbit(x)
E Spec, 18
20 Pet(x)
Split, 19
21 Rabbit(x)
Split, 19
Applying Major Premise...
22 Rabbit(x) => Furry(x)
U Spec, 17
23 Furry(x)
Detach, 22, 21
Joining results...
24 Pet(x) & Furry(x)
Join, 20, 23
Conclusion:
25 EXIST(a):[Pet(a) & Furry(a)]
E Gen, 24
Ferio (EIO-1)
*************
No homework is fun
Some reading is homework
------------------------
Some reading is not fun
Major Premise:
26 ALL(a):[Homework(a) => ~Fun(a)]
Premise
Minor Premise:
27 EXIST(a):[Reading(a) & Homework(a)]
Premise
Applying Minor Premise...
28 Reading(y) & Homework(y)
E Spec, 27
29 Reading(y)
Split, 28
30 Homework(y)
Split, 28
Applying Major Premise...
31 Homework(y) => ~Fun(y)
U Spec, 26
32 ~Fun(y)
Detach, 31, 30
Combining results...
33 Reading(y) & ~Fun(y)
Join, 29, 32
Conclusion:
34 EXIST(a):[Reading(a) & ~Fun(a)]
E Gen, 33