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