5 |
5 |
6 First-Order Logic: quantifier examples (intuitionistic and classical) |
6 First-Order Logic: quantifier examples (intuitionistic and classical) |
7 Needs declarations of the theory "thy" and the tactic "tac" |
7 Needs declarations of the theory "thy" and the tactic "tac" |
8 *) |
8 *) |
9 |
9 |
10 writeln"File FOLP/ex/quant.ML"; |
|
11 |
|
12 Goal "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))"; |
10 Goal "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))"; |
13 by tac; |
11 by tac; |
14 result(); |
12 result(); |
15 |
13 |
16 |
14 |
17 Goal "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"; |
15 Goal "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"; |
18 by tac; |
16 by tac; |
19 result(); |
17 result(); |
20 |
18 |
21 |
19 |
22 (*Converse is false*) |
20 (*Converse is false*) |
23 Goal "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"; |
21 Goal "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"; |
24 by tac; |
22 by tac; |
25 result(); |
23 result(); |
26 |
24 |
27 Goal "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))"; |
25 Goal "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))"; |
28 by tac; |
26 by tac; |
29 result(); |
27 result(); |
30 |
28 |
31 |
29 |
32 Goal "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"; |
30 Goal "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"; |
33 by tac; |
31 by tac; |
34 result(); |
32 result(); |
35 |
33 |
36 |
34 |
37 writeln"Some harder ones"; |
35 writeln"Some harder ones"; |
38 |
36 |
39 Goal "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"; |
37 Goal "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"; |
40 by tac; |
38 by tac; |
41 result(); |
39 result(); |
42 (*6 secs*) |
40 (*6 secs*) |
43 |
41 |
44 (*Converse is false*) |
42 (*Converse is false*) |
45 Goal "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"; |
43 Goal "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"; |
46 by tac; |
44 by tac; |
47 result(); |
45 result(); |
48 |
46 |
49 |
47 |
50 writeln"Basic test of quantifier reasoning"; |
48 writeln"Basic test of quantifier reasoning"; |
51 (*TRUE*) |
49 (*TRUE*) |
52 Goal "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; |
50 Goal "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; |
53 by tac; |
51 by tac; |
54 result(); |
52 result(); |
55 |
53 |
56 |
54 |
57 Goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))"; |
55 Goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))"; |
58 by tac; |
56 by tac; |
59 result(); |
57 result(); |
60 |
58 |
61 |
59 |
62 writeln"The following should fail, as they are false!"; |
60 writeln"The following should fail, as they are false!"; |
63 |
61 |
64 Goal "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"; |
62 Goal "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"; |
65 by tac handle ERROR => writeln"Failed, as expected"; |
63 by tac handle ERROR => writeln"Failed, as expected"; |
66 (*Check that subgoals remain: proof failed.*) |
64 (*Check that subgoals remain: proof failed.*) |
67 getgoal 1; |
65 getgoal 1; |
68 |
66 |
69 Goal "?p : (EX x. Q(x)) --> (ALL x. Q(x))"; |
67 Goal "?p : (EX x. Q(x)) --> (ALL x. Q(x))"; |
70 by tac handle ERROR => writeln"Failed, as expected"; |
68 by tac handle ERROR => writeln"Failed, as expected"; |
71 getgoal 1; |
69 getgoal 1; |
72 |
70 |
73 Goal "?p : P(?a) --> (ALL x. P(x))"; |
71 Goal "?p : P(?a) --> (ALL x. P(x))"; |
74 by tac handle ERROR => writeln"Failed, as expected"; |
72 by tac handle ERROR => writeln"Failed, as expected"; |
75 (*Check that subgoals remain: proof failed.*) |
73 (*Check that subgoals remain: proof failed.*) |
76 getgoal 1; |
74 getgoal 1; |
77 |
75 |
78 Goal |
76 Goal |
79 "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"; |
77 "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"; |
80 by tac handle ERROR => writeln"Failed, as expected"; |
78 by tac handle ERROR => writeln"Failed, as expected"; |
81 getgoal 1; |
79 getgoal 1; |
82 |
80 |
83 |
81 |
84 writeln"Back to things that are provable..."; |
82 writeln"Back to things that are provable..."; |
85 |
83 |
86 Goal "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"; |
84 Goal "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"; |
87 by tac; |
85 by tac; |
88 result(); |
86 result(); |
89 |
87 |
90 |
88 |
91 (*An example of why exI should be delayed as long as possible*) |
89 (*An example of why exI should be delayed as long as possible*) |
92 Goal "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"; |
90 Goal "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"; |
93 by tac; |
91 by tac; |
94 result(); |
92 result(); |
95 |
93 |
96 Goal "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"; |
94 Goal "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"; |
97 by tac; |
95 by tac; |
98 (*Verify that no subgoals remain.*) |
96 (*Verify that no subgoals remain.*) |
99 uresult(); |
97 uresult(); |
100 |
98 |
101 |
99 |
102 Goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))"; |
100 Goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))"; |
103 by tac; |
101 by tac; |
104 result(); |
102 result(); |
105 |
103 |
106 |
104 |
107 writeln"Some slow ones"; |
105 writeln"Some slow ones"; |
108 |
106 |
109 |
107 |
110 (*Principia Mathematica *11.53 *) |
108 (*Principia Mathematica *11.53 *) |
111 Goal "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"; |
109 Goal "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"; |
112 by tac; |
110 by tac; |
113 result(); |
111 result(); |
114 (*6 secs*) |
112 (*6 secs*) |
115 |
113 |
116 (*Principia Mathematica *11.55 *) |
114 (*Principia Mathematica *11.55 *) |
117 Goal "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"; |
115 Goal "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"; |
118 by tac; |
116 by tac; |
119 result(); |
117 result(); |
120 (*9 secs*) |
118 (*9 secs*) |
121 |
119 |
122 (*Principia Mathematica *11.61 *) |
120 (*Principia Mathematica *11.61 *) |
123 Goal "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"; |
121 Goal "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"; |
124 by tac; |
122 by tac; |
125 result(); |
123 result(); |
126 (*3 secs*) |
124 (*3 secs*) |
127 |
|
128 writeln"Reached end of file."; |
|
129 |
|