22 The latter is intuitionistically equivalent to ~~Q-->~~P, hence to ~~P, since |
22 The latter is intuitionistically equivalent to ~~Q-->~~P, hence to ~~P, since |
23 ~~Q is intuitionistically provable. Finally, if P is a negation then ~~P is |
23 ~~Q is intuitionistically provable. Finally, if P is a negation then ~~P is |
24 intuitionstically equivalent to P. [Andy Pitts] *) |
24 intuitionstically equivalent to P. [Andy Pitts] *) |
25 |
25 |
26 lemma "(~~(P&Q)) = ((~~P) & (~~Q))" |
26 lemma "(~~(P&Q)) = ((~~P) & (~~Q))" |
27 by rules |
27 by iprover |
28 |
28 |
29 lemma "~~ ((~P --> Q) --> (~P --> ~Q) --> P)" |
29 lemma "~~ ((~P --> Q) --> (~P --> ~Q) --> P)" |
30 by rules |
30 by iprover |
31 |
31 |
32 (* ~~ does NOT distribute over | *) |
32 (* ~~ does NOT distribute over | *) |
33 |
33 |
34 lemma "(~~(P-->Q)) = (~~P --> ~~Q)" |
34 lemma "(~~(P-->Q)) = (~~P --> ~~Q)" |
35 by rules |
35 by iprover |
36 |
36 |
37 lemma "(~~~P) = (~P)" |
37 lemma "(~~~P) = (~P)" |
38 by rules |
38 by iprover |
39 |
39 |
40 lemma "~~((P --> Q | R) --> (P-->Q) | (P-->R))" |
40 lemma "~~((P --> Q | R) --> (P-->Q) | (P-->R))" |
41 by rules |
41 by iprover |
42 |
42 |
43 lemma "(P=Q) = (Q=P)" |
43 lemma "(P=Q) = (Q=P)" |
44 by rules |
44 by iprover |
45 |
45 |
46 lemma "((P --> (Q | (Q-->R))) --> R) --> R" |
46 lemma "((P --> (Q | (Q-->R))) --> R) --> R" |
47 by rules |
47 by iprover |
48 |
48 |
49 lemma "(((G-->A) --> J) --> D --> E) --> (((H-->B)-->I)-->C-->J) |
49 lemma "(((G-->A) --> J) --> D --> E) --> (((H-->B)-->I)-->C-->J) |
50 --> (A-->H) --> F --> G --> (((C-->B)-->I)-->D)-->(A-->C) |
50 --> (A-->H) --> F --> G --> (((C-->B)-->I)-->D)-->(A-->C) |
51 --> (((F-->A)-->B) --> I) --> E" |
51 --> (((F-->A)-->B) --> I) --> E" |
52 by rules |
52 by iprover |
53 |
53 |
54 |
54 |
55 (* Lemmas for the propositional double-negation translation *) |
55 (* Lemmas for the propositional double-negation translation *) |
56 |
56 |
57 lemma "P --> ~~P" |
57 lemma "P --> ~~P" |
58 by rules |
58 by iprover |
59 |
59 |
60 lemma "~~(~~P --> P)" |
60 lemma "~~(~~P --> P)" |
61 by rules |
61 by iprover |
62 |
62 |
63 lemma "~~P & ~~(P --> Q) --> ~~Q" |
63 lemma "~~P & ~~(P --> Q) --> ~~Q" |
64 by rules |
64 by iprover |
65 |
65 |
66 |
66 |
67 (* de Bruijn formulae *) |
67 (* de Bruijn formulae *) |
68 |
68 |
69 (*de Bruijn formula with three predicates*) |
69 (*de Bruijn formula with three predicates*) |
70 lemma "((P=Q) --> P&Q&R) & |
70 lemma "((P=Q) --> P&Q&R) & |
71 ((Q=R) --> P&Q&R) & |
71 ((Q=R) --> P&Q&R) & |
72 ((R=P) --> P&Q&R) --> P&Q&R" |
72 ((R=P) --> P&Q&R) --> P&Q&R" |
73 by rules |
73 by iprover |
74 |
74 |
75 (*de Bruijn formula with five predicates*) |
75 (*de Bruijn formula with five predicates*) |
76 lemma "((P=Q) --> P&Q&R&S&T) & |
76 lemma "((P=Q) --> P&Q&R&S&T) & |
77 ((Q=R) --> P&Q&R&S&T) & |
77 ((Q=R) --> P&Q&R&S&T) & |
78 ((R=S) --> P&Q&R&S&T) & |
78 ((R=S) --> P&Q&R&S&T) & |
79 ((S=T) --> P&Q&R&S&T) & |
79 ((S=T) --> P&Q&R&S&T) & |
80 ((T=P) --> P&Q&R&S&T) --> P&Q&R&S&T" |
80 ((T=P) --> P&Q&R&S&T) --> P&Q&R&S&T" |
81 by rules |
81 by iprover |
82 |
82 |
83 |
83 |
84 (*** Problems from Sahlin, Franzen and Haridi, |
84 (*** Problems from Sahlin, Franzen and Haridi, |
85 An Intuitionistic Predicate Logic Theorem Prover. |
85 An Intuitionistic Predicate Logic Theorem Prover. |
86 J. Logic and Comp. 2 (5), October 1992, 619-656. |
86 J. Logic and Comp. 2 (5), October 1992, 619-656. |
87 ***) |
87 ***) |
88 |
88 |
89 (*Problem 1.1*) |
89 (*Problem 1.1*) |
90 lemma "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) = |
90 lemma "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) = |
91 (ALL z. EX y. ALL x. p(x) & q(y) & r(z))" |
91 (ALL z. EX y. ALL x. p(x) & q(y) & r(z))" |
92 by (rules del: allE elim 2: allE') |
92 by (iprover del: allE elim 2: allE') |
93 |
93 |
94 (*Problem 3.1*) |
94 (*Problem 3.1*) |
95 lemma "~ (EX x. ALL y. p y x = (~ p x x))" |
95 lemma "~ (EX x. ALL y. p y x = (~ p x x))" |
96 by rules |
96 by iprover |
97 |
97 |
98 |
98 |
99 (* Intuitionistic FOL: propositional problems based on Pelletier. *) |
99 (* Intuitionistic FOL: propositional problems based on Pelletier. *) |
100 |
100 |
101 (* Problem ~~1 *) |
101 (* Problem ~~1 *) |
102 lemma "~~((P-->Q) = (~Q --> ~P))" |
102 lemma "~~((P-->Q) = (~Q --> ~P))" |
103 by rules |
103 by iprover |
104 |
104 |
105 (* Problem ~~2 *) |
105 (* Problem ~~2 *) |
106 lemma "~~(~~P = P)" |
106 lemma "~~(~~P = P)" |
107 by rules |
107 by iprover |
108 |
108 |
109 (* Problem 3 *) |
109 (* Problem 3 *) |
110 lemma "~(P-->Q) --> (Q-->P)" |
110 lemma "~(P-->Q) --> (Q-->P)" |
111 by rules |
111 by iprover |
112 |
112 |
113 (* Problem ~~4 *) |
113 (* Problem ~~4 *) |
114 lemma "~~((~P-->Q) = (~Q --> P))" |
114 lemma "~~((~P-->Q) = (~Q --> P))" |
115 by rules |
115 by iprover |
116 |
116 |
117 (* Problem ~~5 *) |
117 (* Problem ~~5 *) |
118 lemma "~~((P|Q-->P|R) --> P|(Q-->R))" |
118 lemma "~~((P|Q-->P|R) --> P|(Q-->R))" |
119 by rules |
119 by iprover |
120 |
120 |
121 (* Problem ~~6 *) |
121 (* Problem ~~6 *) |
122 lemma "~~(P | ~P)" |
122 lemma "~~(P | ~P)" |
123 by rules |
123 by iprover |
124 |
124 |
125 (* Problem ~~7 *) |
125 (* Problem ~~7 *) |
126 lemma "~~(P | ~~~P)" |
126 lemma "~~(P | ~~~P)" |
127 by rules |
127 by iprover |
128 |
128 |
129 (* Problem ~~8. Peirce's law *) |
129 (* Problem ~~8. Peirce's law *) |
130 lemma "~~(((P-->Q) --> P) --> P)" |
130 lemma "~~(((P-->Q) --> P) --> P)" |
131 by rules |
131 by iprover |
132 |
132 |
133 (* Problem 9 *) |
133 (* Problem 9 *) |
134 lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" |
134 lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" |
135 by rules |
135 by iprover |
136 |
136 |
137 (* Problem 10 *) |
137 (* Problem 10 *) |
138 lemma "(Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P=Q)" |
138 lemma "(Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P=Q)" |
139 by rules |
139 by iprover |
140 |
140 |
141 (* 11. Proved in each direction (incorrectly, says Pelletier!!) *) |
141 (* 11. Proved in each direction (incorrectly, says Pelletier!!) *) |
142 lemma "P=P" |
142 lemma "P=P" |
143 by rules |
143 by iprover |
144 |
144 |
145 (* Problem ~~12. Dijkstra's law *) |
145 (* Problem ~~12. Dijkstra's law *) |
146 lemma "~~(((P = Q) = R) = (P = (Q = R)))" |
146 lemma "~~(((P = Q) = R) = (P = (Q = R)))" |
147 by rules |
147 by iprover |
148 |
148 |
149 lemma "((P = Q) = R) --> ~~(P = (Q = R))" |
149 lemma "((P = Q) = R) --> ~~(P = (Q = R))" |
150 by rules |
150 by iprover |
151 |
151 |
152 (* Problem 13. Distributive law *) |
152 (* Problem 13. Distributive law *) |
153 lemma "(P | (Q & R)) = ((P | Q) & (P | R))" |
153 lemma "(P | (Q & R)) = ((P | Q) & (P | R))" |
154 by rules |
154 by iprover |
155 |
155 |
156 (* Problem ~~14 *) |
156 (* Problem ~~14 *) |
157 lemma "~~((P = Q) = ((Q | ~P) & (~Q|P)))" |
157 lemma "~~((P = Q) = ((Q | ~P) & (~Q|P)))" |
158 by rules |
158 by iprover |
159 |
159 |
160 (* Problem ~~15 *) |
160 (* Problem ~~15 *) |
161 lemma "~~((P --> Q) = (~P | Q))" |
161 lemma "~~((P --> Q) = (~P | Q))" |
162 by rules |
162 by iprover |
163 |
163 |
164 (* Problem ~~16 *) |
164 (* Problem ~~16 *) |
165 lemma "~~((P-->Q) | (Q-->P))" |
165 lemma "~~((P-->Q) | (Q-->P))" |
166 by rules |
166 by iprover |
167 |
167 |
168 (* Problem ~~17 *) |
168 (* Problem ~~17 *) |
169 lemma "~~(((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S)))" |
169 lemma "~~(((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S)))" |
170 oops |
170 oops |
171 |
171 |
172 (*Dijkstra's "Golden Rule"*) |
172 (*Dijkstra's "Golden Rule"*) |
173 lemma "(P&Q) = (P = (Q = (P|Q)))" |
173 lemma "(P&Q) = (P = (Q = (P|Q)))" |
174 by rules |
174 by iprover |
175 |
175 |
176 |
176 |
177 (****Examples with quantifiers****) |
177 (****Examples with quantifiers****) |
178 |
178 |
179 (* The converse is classical in the following implications... *) |
179 (* The converse is classical in the following implications... *) |
180 |
180 |
181 lemma "(EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q" |
181 lemma "(EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q" |
182 by rules |
182 by iprover |
183 |
183 |
184 lemma "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)" |
184 lemma "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)" |
185 by rules |
185 by iprover |
186 |
186 |
187 lemma "((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))" |
187 lemma "((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))" |
188 by rules |
188 by iprover |
189 |
189 |
190 lemma "(ALL x. P(x)) | Q --> (ALL x. P(x) | Q)" |
190 lemma "(ALL x. P(x)) | Q --> (ALL x. P(x) | Q)" |
191 by rules |
191 by iprover |
192 |
192 |
193 lemma "(EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))" |
193 lemma "(EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))" |
194 by rules |
194 by iprover |
195 |
195 |
196 |
196 |
197 (* Hard examples with quantifiers *) |
197 (* Hard examples with quantifiers *) |
198 |
198 |
199 (*The ones that have not been proved are not known to be valid! |
199 (*The ones that have not been proved are not known to be valid! |
200 Some will require quantifier duplication -- not currently available*) |
200 Some will require quantifier duplication -- not currently available*) |
201 |
201 |
202 (* Problem ~~19 *) |
202 (* Problem ~~19 *) |
203 lemma "~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" |
203 lemma "~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" |
204 by rules |
204 by iprover |
205 |
205 |
206 (* Problem 20 *) |
206 (* Problem 20 *) |
207 lemma "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) |
207 lemma "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) |
208 --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))" |
208 --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))" |
209 by rules |
209 by iprover |
210 |
210 |
211 (* Problem 21 *) |
211 (* Problem 21 *) |
212 lemma "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P=Q(x))" |
212 lemma "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P=Q(x))" |
213 by rules |
213 by iprover |
214 |
214 |
215 (* Problem 22 *) |
215 (* Problem 22 *) |
216 lemma "(ALL x. P = Q(x)) --> (P = (ALL x. Q(x)))" |
216 lemma "(ALL x. P = Q(x)) --> (P = (ALL x. Q(x)))" |
217 by rules |
217 by iprover |
218 |
218 |
219 (* Problem ~~23 *) |
219 (* Problem ~~23 *) |
220 lemma "~~ ((ALL x. P | Q(x)) = (P | (ALL x. Q(x))))" |
220 lemma "~~ ((ALL x. P | Q(x)) = (P | (ALL x. Q(x))))" |
221 by rules |
221 by iprover |
222 |
222 |
223 (* Problem 25 *) |
223 (* Problem 25 *) |
224 lemma "(EX x. P(x)) & |
224 lemma "(EX x. P(x)) & |
225 (ALL x. L(x) --> ~ (M(x) & R(x))) & |
225 (ALL x. L(x) --> ~ (M(x) & R(x))) & |
226 (ALL x. P(x) --> (M(x) & L(x))) & |
226 (ALL x. P(x) --> (M(x) & L(x))) & |
227 ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) |
227 ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) |
228 --> (EX x. Q(x)&P(x))" |
228 --> (EX x. Q(x)&P(x))" |
229 by rules |
229 by iprover |
230 |
230 |
231 (* Problem 27 *) |
231 (* Problem 27 *) |
232 lemma "(EX x. P(x) & ~Q(x)) & |
232 lemma "(EX x. P(x) & ~Q(x)) & |
233 (ALL x. P(x) --> R(x)) & |
233 (ALL x. P(x) --> R(x)) & |
234 (ALL x. M(x) & L(x) --> P(x)) & |
234 (ALL x. M(x) & L(x) --> P(x)) & |
235 ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) |
235 ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) |
236 --> (ALL x. M(x) --> ~L(x))" |
236 --> (ALL x. M(x) --> ~L(x))" |
237 by rules |
237 by iprover |
238 |
238 |
239 (* Problem ~~28. AMENDED *) |
239 (* Problem ~~28. AMENDED *) |
240 lemma "(ALL x. P(x) --> (ALL x. Q(x))) & |
240 lemma "(ALL x. P(x) --> (ALL x. Q(x))) & |
241 (~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & |
241 (~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & |
242 (~~(EX x. S(x)) --> (ALL x. L(x) --> M(x))) |
242 (~~(EX x. S(x)) --> (ALL x. L(x) --> M(x))) |
243 --> (ALL x. P(x) & L(x) --> M(x))" |
243 --> (ALL x. P(x) & L(x) --> M(x))" |
244 by rules |
244 by iprover |
245 |
245 |
246 (* Problem 29. Essentially the same as Principia Mathematica *11.71 *) |
246 (* Problem 29. Essentially the same as Principia Mathematica *11.71 *) |
247 lemma "(((EX x. P(x)) & (EX y. Q(y))) --> |
247 lemma "(((EX x. P(x)) & (EX y. Q(y))) --> |
248 (((ALL x. (P(x) --> R(x))) & (ALL y. (Q(y) --> S(y)))) = |
248 (((ALL x. (P(x) --> R(x))) & (ALL y. (Q(y) --> S(y)))) = |
249 (ALL x y. ((P(x) & Q(y)) --> (R(x) & S(y))))))" |
249 (ALL x y. ((P(x) & Q(y)) --> (R(x) & S(y))))))" |
250 by rules |
250 by iprover |
251 |
251 |
252 (* Problem ~~30 *) |
252 (* Problem ~~30 *) |
253 lemma "(ALL x. (P(x) | Q(x)) --> ~ R(x)) & |
253 lemma "(ALL x. (P(x) | Q(x)) --> ~ R(x)) & |
254 (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) |
254 (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) |
255 --> (ALL x. ~~S(x))" |
255 --> (ALL x. ~~S(x))" |
256 by rules |
256 by iprover |
257 |
257 |
258 (* Problem 31 *) |
258 (* Problem 31 *) |
259 lemma "~(EX x. P(x) & (Q(x) | R(x))) & |
259 lemma "~(EX x. P(x) & (Q(x) | R(x))) & |
260 (EX x. L(x) & P(x)) & |
260 (EX x. L(x) & P(x)) & |
261 (ALL x. ~ R(x) --> M(x)) |
261 (ALL x. ~ R(x) --> M(x)) |
262 --> (EX x. L(x) & M(x))" |
262 --> (EX x. L(x) & M(x))" |
263 by rules |
263 by iprover |
264 |
264 |
265 (* Problem 32 *) |
265 (* Problem 32 *) |
266 lemma "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) & |
266 lemma "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) & |
267 (ALL x. S(x) & R(x) --> L(x)) & |
267 (ALL x. S(x) & R(x) --> L(x)) & |
268 (ALL x. M(x) --> R(x)) |
268 (ALL x. M(x) --> R(x)) |
269 --> (ALL x. P(x) & M(x) --> L(x))" |
269 --> (ALL x. P(x) & M(x) --> L(x))" |
270 by rules |
270 by iprover |
271 |
271 |
272 (* Problem ~~33 *) |
272 (* Problem ~~33 *) |
273 lemma "(ALL x. ~~(P(a) & (P(x)-->P(b))-->P(c))) = |
273 lemma "(ALL x. ~~(P(a) & (P(x)-->P(b))-->P(c))) = |
274 (ALL x. ~~((~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c))))" |
274 (ALL x. ~~((~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c))))" |
275 oops |
275 oops |
278 lemma |
278 lemma |
279 "(ALL x. EX y. J x y) & |
279 "(ALL x. EX y. J x y) & |
280 (ALL x. EX y. G x y) & |
280 (ALL x. EX y. G x y) & |
281 (ALL x y. J x y | G x y --> (ALL z. J y z | G y z --> H x z)) |
281 (ALL x y. J x y | G x y --> (ALL z. J y z | G y z --> H x z)) |
282 --> (ALL x. EX y. H x y)" |
282 --> (ALL x. EX y. H x y)" |
283 by rules |
283 by iprover |
284 |
284 |
285 (* Problem 39 *) |
285 (* Problem 39 *) |
286 lemma "~ (EX x. ALL y. F y x = (~F y y))" |
286 lemma "~ (EX x. ALL y. F y x = (~F y y))" |
287 by rules |
287 by iprover |
288 |
288 |
289 (* Problem 40. AMENDED *) |
289 (* Problem 40. AMENDED *) |
290 lemma "(EX y. ALL x. F x y = F x x) --> |
290 lemma "(EX y. ALL x. F x y = F x x) --> |
291 ~(ALL x. EX y. ALL z. F z y = (~ F z x))" |
291 ~(ALL x. EX y. ALL z. F z y = (~ F z x))" |
292 by rules |
292 by iprover |
293 |
293 |
294 (* Problem 44 *) |
294 (* Problem 44 *) |
295 lemma "(ALL x. f(x) --> |
295 lemma "(ALL x. f(x) --> |
296 (EX y. g(y) & h x y & (EX y. g(y) & ~ h x y))) & |
296 (EX y. g(y) & h x y & (EX y. g(y) & ~ h x y))) & |
297 (EX x. j(x) & (ALL y. g(y) --> h x y)) |
297 (EX x. j(x) & (ALL y. g(y) --> h x y)) |
298 --> (EX x. j(x) & ~f(x))" |
298 --> (EX x. j(x) & ~f(x))" |
299 by rules |
299 by iprover |
300 |
300 |
301 (* Problem 48 *) |
301 (* Problem 48 *) |
302 lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c" |
302 lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c" |
303 by rules |
303 by iprover |
304 |
304 |
305 (* Problem 51 *) |
305 (* Problem 51 *) |
306 lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) --> |
306 lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) --> |
307 (EX z. (ALL x. (EX w. ((ALL y. (P x y = (y = w))) = (x = z))))))" |
307 (EX z. (ALL x. (EX w. ((ALL y. (P x y = (y = w))) = (x = z))))))" |
308 by rules |
308 by iprover |
309 |
309 |
310 (* Problem 52 *) |
310 (* Problem 52 *) |
311 (*Almost the same as 51. *) |
311 (*Almost the same as 51. *) |
312 lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) --> |
312 lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) --> |
313 (EX w. (ALL y. (EX z. ((ALL x. (P x y = (x = z))) = (y = w))))))" |
313 (EX w. (ALL y. (EX z. ((ALL x. (P x y = (x = z))) = (y = w))))))" |
314 by rules |
314 by iprover |
315 |
315 |
316 (* Problem 56 *) |
316 (* Problem 56 *) |
317 lemma "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) = (ALL x. P(x) --> P(f(x)))" |
317 lemma "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) = (ALL x. P(x) --> P(f(x)))" |
318 by rules |
318 by iprover |
319 |
319 |
320 (* Problem 57 *) |
320 (* Problem 57 *) |
321 lemma "P (f a b) (f b c) & P (f b c) (f a c) & |
321 lemma "P (f a b) (f b c) & P (f b c) (f a c) & |
322 (ALL x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)" |
322 (ALL x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)" |
323 by rules |
323 by iprover |
324 |
324 |
325 (* Problem 60 *) |
325 (* Problem 60 *) |
326 lemma "ALL x. P x (f x) = (EX y. (ALL z. P z y --> P z (f x)) & P x y)" |
326 lemma "ALL x. P x (f x) = (EX y. (ALL z. P z y --> P z (f x)) & P x y)" |
327 by rules |
327 by iprover |
328 |
328 |
329 end |
329 end |