author  nipkow 
Thu, 22 Sep 2005 23:56:15 +0200  
changeset 17589  58eeffd73be1 
parent 17388  495c799df31d 
child 41460  ea56b98aee83 
permissions  rwrr 
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 
ID: $Id$ 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

4 
Copyright 1991 University of Cambridge 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

5 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

6 
Taken from FOL/ex/int.ML 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

7 
*) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

8 

17388  9 
header {* HigherOrder Logic: Intuitionistic predicate calculus problems *} 
10 

16417  11 
theory Intuitionistic imports Main begin 
12450
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 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

14 
(*Metatheorem (for PROPOSITIONAL formulae...): 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

15 
P is classically provable iff ~~P is intuitionistically provable. 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

16 
Therefore ~P is classically provable iff it is intuitionistically provable. 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

17 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

18 
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

19 
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

20 
~~ 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

21 
provable intuitionistically, so ~~(Q>P) is also provable intuitionistically. 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

22 
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

23 
~~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

24 
intuitionstically equivalent to P. [Andy Pitts] *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

25 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

26 
lemma "(~~(P&Q)) = ((~~P) & (~~Q))" 
17589  27 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

28 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

29 
lemma "~~ ((~P > Q) > (~P > ~Q) > P)" 
17589  30 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

31 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

32 
(* ~~ does NOT distribute over  *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

33 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

34 
lemma "(~~(P>Q)) = (~~P > ~~Q)" 
17589  35 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

36 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

37 
lemma "(~~~P) = (~P)" 
17589  38 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

39 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

40 
lemma "~~((P > Q  R) > (P>Q)  (P>R))" 
17589  41 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

42 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

43 
lemma "(P=Q) = (Q=P)" 
17589  44 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

45 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

46 
lemma "((P > (Q  (Q>R))) > R) > R" 
17589  47 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

48 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

49 
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

50 
> (A>H) > F > G > (((C>B)>I)>D)>(A>C) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

51 
> (((F>A)>B) > I) > E" 
17589  52 
by iprover 
12450
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 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

55 
(* Lemmas for the propositional doublenegation translation *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

56 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

57 
lemma "P > ~~P" 
17589  58 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

59 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

60 
lemma "~~(~~P > P)" 
17589  61 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

62 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

63 
lemma "~~P & ~~(P > Q) > ~~Q" 
17589  64 
by iprover 
12450
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 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

67 
(* de Bruijn formulae *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

68 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

69 
(*de Bruijn formula with three predicates*) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

70 
lemma "((P=Q) > P&Q&R) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

71 
((Q=R) > P&Q&R) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

72 
((R=P) > P&Q&R) > P&Q&R" 
17589  73 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

74 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

75 
(*de Bruijn formula with five predicates*) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

76 
lemma "((P=Q) > P&Q&R&S&T) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

77 
((Q=R) > P&Q&R&S&T) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

78 
((R=S) > P&Q&R&S&T) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

79 
((S=T) > P&Q&R&S&T) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

80 
((T=P) > P&Q&R&S&T) > P&Q&R&S&T" 
17589  81 
by iprover 
12450
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 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

84 
(*** Problems from Sahlin, Franzen and Haridi, 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

85 
An Intuitionistic Predicate Logic Theorem Prover. 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

86 
J. Logic and Comp. 2 (5), October 1992, 619656. 
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 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

89 
(*Problem 1.1*) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

90 
lemma "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) = 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

91 
(ALL z. EX y. ALL x. p(x) & q(y) & r(z))" 
17589  92 
by (iprover del: allE elim 2: allE') 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

93 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

94 
(*Problem 3.1*) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

95 
lemma "~ (EX x. ALL y. p y x = (~ p x x))" 
17589  96 
by iprover 
12450
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 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

99 
(* Intuitionistic FOL: propositional problems based on Pelletier. *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

100 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

101 
(* Problem ~~1 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

102 
lemma "~~((P>Q) = (~Q > ~P))" 
17589  103 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

104 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

105 
(* Problem ~~2 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

106 
lemma "~~(~~P = P)" 
17589  107 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

108 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

109 
(* Problem 3 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

110 
lemma "~(P>Q) > (Q>P)" 
17589  111 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

112 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

113 
(* Problem ~~4 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

114 
lemma "~~((~P>Q) = (~Q > P))" 
17589  115 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

116 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

117 
(* Problem ~~5 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

118 
lemma "~~((PQ>PR) > P(Q>R))" 
17589  119 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

120 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

121 
(* Problem ~~6 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

122 
lemma "~~(P  ~P)" 
17589  123 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

124 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

125 
(* Problem ~~7 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

126 
lemma "~~(P  ~~~P)" 
17589  127 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

128 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

129 
(* Problem ~~8. Peirce's law *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

130 
lemma "~~(((P>Q) > P) > P)" 
17589  131 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

132 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

133 
(* Problem 9 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

134 
lemma "((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)" 
17589  135 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

136 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

137 
(* Problem 10 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

138 
lemma "(Q>R) > (R>P&Q) > (P>(QR)) > (P=Q)" 
17589  139 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

140 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

141 
(* 11. Proved in each direction (incorrectly, says Pelletier!!) *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

142 
lemma "P=P" 
17589  143 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

144 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

145 
(* Problem ~~12. Dijkstra's law *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

146 
lemma "~~(((P = Q) = R) = (P = (Q = R)))" 
17589  147 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

148 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

149 
lemma "((P = Q) = R) > ~~(P = (Q = R))" 
17589  150 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

151 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

152 
(* Problem 13. Distributive law *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

153 
lemma "(P  (Q & R)) = ((P  Q) & (P  R))" 
17589  154 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

155 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

156 
(* Problem ~~14 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

157 
lemma "~~((P = Q) = ((Q  ~P) & (~QP)))" 
17589  158 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

159 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

160 
(* Problem ~~15 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

161 
lemma "~~((P > Q) = (~P  Q))" 
17589  162 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

163 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

164 
(* Problem ~~16 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

165 
lemma "~~((P>Q)  (Q>P))" 
17589  166 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

167 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

168 
(* Problem ~~17 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

169 
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

170 
oops 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

171 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

172 
(*Dijkstra's "Golden Rule"*) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

173 
lemma "(P&Q) = (P = (Q = (PQ)))" 
17589  174 
by iprover 
12450
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 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

177 
(****Examples with quantifiers****) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

178 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

179 
(* The converse is classical in the following implications... *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

180 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

181 
lemma "(EX x. P(x)>Q) > (ALL x. P(x)) > Q" 
17589  182 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

183 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

184 
lemma "((ALL x. P(x))>Q) > ~ (ALL x. P(x) & ~Q)" 
17589  185 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

186 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

187 
lemma "((ALL x. ~P(x))>Q) > ~ (ALL x. ~ (P(x)Q))" 
17589  188 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

189 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

190 
lemma "(ALL x. P(x))  Q > (ALL x. P(x)  Q)" 
17589  191 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

192 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

193 
lemma "(EX x. P > Q(x)) > (P > (EX x. Q(x)))" 
17589  194 
by iprover 
12450
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 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

197 
(* Hard examples with quantifiers *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

198 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

199 
(*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

200 
Some will require quantifier duplication  not currently available*) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

201 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

202 
(* Problem ~~19 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

203 
lemma "~~(EX x. ALL y z. (P(y)>Q(z)) > (P(x)>Q(x)))" 
17589  204 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

205 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

206 
(* Problem 20 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

207 
lemma "(ALL x y. EX z. ALL w. (P(x)&Q(y)>R(z)&S(w))) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

208 
> (EX x y. P(x) & Q(y)) > (EX z. R(z))" 
17589  209 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

210 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

211 
(* Problem 21 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

212 
lemma "(EX x. P>Q(x)) & (EX x. Q(x)>P) > ~~(EX x. P=Q(x))" 
17589  213 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

214 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

215 
(* Problem 22 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

216 
lemma "(ALL x. P = Q(x)) > (P = (ALL x. Q(x)))" 
17589  217 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

218 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

219 
(* Problem ~~23 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

220 
lemma "~~ ((ALL x. P  Q(x)) = (P  (ALL x. Q(x))))" 
17589  221 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

222 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

223 
(* Problem 25 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

224 
lemma "(EX x. P(x)) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

225 
(ALL x. L(x) > ~ (M(x) & R(x))) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

226 
(ALL x. P(x) > (M(x) & L(x))) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

227 
((ALL x. P(x)>Q(x))  (EX x. P(x)&R(x))) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

228 
> (EX x. Q(x)&P(x))" 
17589  229 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

230 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

231 
(* Problem 27 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

232 
lemma "(EX x. P(x) & ~Q(x)) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

233 
(ALL x. P(x) > R(x)) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

234 
(ALL x. M(x) & L(x) > P(x)) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

235 
((EX x. R(x) & ~ Q(x)) > (ALL x. L(x) > ~ R(x))) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

236 
> (ALL x. M(x) > ~L(x))" 
17589  237 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

238 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

239 
(* Problem ~~28. AMENDED *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

240 
lemma "(ALL x. P(x) > (ALL x. Q(x))) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

241 
(~~(ALL x. Q(x)R(x)) > (EX x. Q(x)&S(x))) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

242 
(~~(EX x. S(x)) > (ALL x. L(x) > M(x))) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

243 
> (ALL x. P(x) & L(x) > M(x))" 
17589  244 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

245 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

246 
(* Problem 29. Essentially the same as Principia Mathematica *11.71 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

247 
lemma "(((EX x. P(x)) & (EX y. Q(y))) > 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

248 
(((ALL x. (P(x) > R(x))) & (ALL y. (Q(y) > S(y)))) = 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

249 
(ALL x y. ((P(x) & Q(y)) > (R(x) & S(y))))))" 
17589  250 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

251 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

252 
(* Problem ~~30 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

253 
lemma "(ALL x. (P(x)  Q(x)) > ~ R(x)) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

254 
(ALL x. (Q(x) > ~ S(x)) > P(x) & R(x)) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

255 
> (ALL x. ~~S(x))" 
17589  256 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

257 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

258 
(* Problem 31 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

259 
lemma "~(EX x. P(x) & (Q(x)  R(x))) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

260 
(EX x. L(x) & P(x)) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

261 
(ALL x. ~ R(x) > M(x)) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

262 
> (EX x. L(x) & M(x))" 
17589  263 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

264 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

265 
(* Problem 32 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

266 
lemma "(ALL x. P(x) & (Q(x)R(x))>S(x)) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

267 
(ALL x. S(x) & R(x) > L(x)) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

268 
(ALL x. M(x) > R(x)) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

269 
> (ALL x. P(x) & M(x) > L(x))" 
17589  270 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

271 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

272 
(* Problem ~~33 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

273 
lemma "(ALL x. ~~(P(a) & (P(x)>P(b))>P(c))) = 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

274 
(ALL x. ~~((~P(a)  P(x)  P(c)) & (~P(a)  ~P(b)  P(c))))" 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

275 
oops 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

276 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

277 
(* Problem 36 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

278 
lemma 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

279 
"(ALL x. EX y. J x y) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

280 
(ALL x. EX y. G x y) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

281 
(ALL x y. J x y  G x y > (ALL z. J y z  G y z > H x z)) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

282 
> (ALL x. EX y. H x y)" 
17589  283 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

284 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

285 
(* Problem 39 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

286 
lemma "~ (EX x. ALL y. F y x = (~F y y))" 
17589  287 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

288 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

289 
(* Problem 40. AMENDED *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

290 
lemma "(EX y. ALL x. F x y = F x x) > 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

291 
~(ALL x. EX y. ALL z. F z y = (~ F z x))" 
17589  292 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

293 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

294 
(* Problem 44 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

295 
lemma "(ALL x. f(x) > 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

296 
(EX y. g(y) & h x y & (EX y. g(y) & ~ h x y))) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

297 
(EX x. j(x) & (ALL y. g(y) > h x y)) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

298 
> (EX x. j(x) & ~f(x))" 
17589  299 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

300 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

301 
(* Problem 48 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

302 
lemma "(a=b  c=d) & (a=c  b=d) > a=d  b=c" 
17589  303 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

304 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

305 
(* Problem 51 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

306 
lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) > 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

307 
(EX z. (ALL x. (EX w. ((ALL y. (P x y = (y = w))) = (x = z))))))" 
17589  308 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

309 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

310 
(* Problem 52 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

311 
(*Almost the same as 51. *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

312 
lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) > 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

313 
(EX w. (ALL y. (EX z. ((ALL x. (P x y = (x = z))) = (y = w))))))" 
17589  314 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

315 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

316 
(* Problem 56 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

317 
lemma "(ALL x. (EX y. P(y) & x=f(y)) > P(x)) = (ALL x. P(x) > P(f(x)))" 
17589  318 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

319 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

320 
(* Problem 57 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

321 
lemma "P (f a b) (f b c) & P (f b c) (f a c) & 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

322 
(ALL x y z. P x y & P y z > P x z) > P (f a b) (f a c)" 
17589  323 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

324 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

325 
(* Problem 60 *) 
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

326 
lemma "ALL x. P x (f x) = (EX y. (ALL z. P z y > P z (f x)) & P x y)" 
17589  327 
by iprover 
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

328 

1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff
changeset

329 
end 