61 |
61 |
62 writeln"The following are classically but not constructively valid."; |
62 writeln"The following are classically but not constructively valid."; |
63 |
63 |
64 (*The attempt to prove them terminates quickly!*) |
64 (*The attempt to prove them terminates quickly!*) |
65 goal (theory "IFOLP") "?p : ((P-->Q) --> P) --> P"; |
65 goal (theory "IFOLP") "?p : ((P-->Q) --> P) --> P"; |
66 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected"; |
66 by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected"; |
67 (*Check that subgoals remain: proof failed.*) |
67 (*Check that subgoals remain: proof failed.*) |
68 getgoal 1; |
68 getgoal 1; |
69 |
69 |
70 goal (theory "IFOLP") "?p : (P&Q-->R) --> (P-->R) | (Q-->R)"; |
70 goal (theory "IFOLP") "?p : (P&Q-->R) --> (P-->R) | (Q-->R)"; |
71 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected"; |
71 by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected"; |
72 getgoal 1; |
72 getgoal 1; |
73 |
73 |
74 |
74 |
75 writeln"Intuitionistic FOL: propositional problems based on Pelletier."; |
75 writeln"Intuitionistic FOL: propositional problems based on Pelletier."; |
76 |
76 |
203 |
203 |
204 writeln"The following are not constructively valid!"; |
204 writeln"The following are not constructively valid!"; |
205 (*The attempt to prove them terminates quickly!*) |
205 (*The attempt to prove them terminates quickly!*) |
206 |
206 |
207 goal (theory "IFOLP") "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"; |
207 goal (theory "IFOLP") "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"; |
208 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected"; |
208 by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected"; |
209 getgoal 1; |
209 getgoal 1; |
210 |
210 |
211 goal (theory "IFOLP") "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"; |
211 goal (theory "IFOLP") "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"; |
212 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected"; |
212 by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected"; |
213 getgoal 1; |
213 getgoal 1; |
214 |
214 |
215 goal (theory "IFOLP") "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"; |
215 goal (theory "IFOLP") "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"; |
216 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected"; |
216 by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected"; |
217 getgoal 1; |
217 getgoal 1; |
218 |
218 |
219 goal (theory "IFOLP") "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))"; |
219 goal (theory "IFOLP") "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))"; |
220 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected"; |
220 by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected"; |
221 getgoal 1; |
221 getgoal 1; |
222 |
222 |
223 (*Classically but not intuitionistically valid. Proved by a bug in 1986!*) |
223 (*Classically but not intuitionistically valid. Proved by a bug in 1986!*) |
224 goal (theory "IFOLP") "?p : EX x. Q(x) --> (ALL x. Q(x))"; |
224 goal (theory "IFOLP") "?p : EX x. Q(x) --> (ALL x. Q(x))"; |
225 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected"; |
225 by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected"; |
226 getgoal 1; |
226 getgoal 1; |
227 |
227 |
228 |
228 |
229 writeln"Hard examples with quantifiers"; |
229 writeln"Hard examples with quantifiers"; |
230 |
230 |