1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
MPC;
alpha . x y z;
PRED alpha alpha . R;
PROOF;
{ all x,y.R x y -> R y x.
{ all x,y,z.R x y -> R y z -> R x z.
{ x.
{ y.
{ R x y.
all y,z.R x y -> R y z -> R x z;
all z.R x y -> R y z -> R x z;
R x y -> R y x -> R x x;
R y x -> R x x;
all y.R x y -> R y x;
R x y -> R y x;
R y x;
R x x;
}
R x y -> R x x;
}
all y.R x y -> R x x;
}
all x,y.R x y -> R x x;
}
(all x,y,z.R x y -> R y z -> R x z) -> all x,y.R x y -> R x x;
}
(all x,y.R x y -> R y x) -> (all x,y,z.R x y -> R y z -> R x z) -> all x,y.R x y -> R x x;
PRED . P;
PRED alpha . Q;
{ ex x Q x -> P.
{ x.
{ Q x.
ex x Q x;
P;
}
Q x ->P;
}
all x.Q x -> P;
}
(ex x Q x -> P) -> all x.Q x -> P;
CLASSIC PROOF;
{ all x.(Q x -> all y Q y) -> F.
(Q x -> all y Q y) -> F;
{ Q x.
{ y.
{ Q y -> F.
{ Q y.
F;
all y Q y;
}
Q y -> all y Q y;
(Q y -> all y Q y) -> F;
F;
}
(Q y -> F) -> F;
Q y;
}
all y Q y;
}
Q x -> all y Q y;
F;
}
exca x.Q x -> all y Q y;
END;
|
