14239

1 
(* Title: FOL/ex/Intuitionistic


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 
*)


6 


7 
header{*Intuitionistic FirstOrder Logic*}


8 

16417

9 
theory Intuitionistic imports IFOL begin

14239

10 


11 
(*


12 
Singlestep ML commands:


13 
by (IntPr.step_tac 1)


14 
by (biresolve_tac safe_brls 1);


15 
by (biresolve_tac haz_brls 1);


16 
by (assume_tac 1);


17 
by (IntPr.safe_tac 1);


18 
by (IntPr.mp_tac 1);


19 
by (IntPr.fast_tac 1);


20 
*)


21 


22 


23 
text{*Metatheorem (for \emph{propositional} formulae):


24 
$P$ is classically provable iff $\neg\neg P$ is intuitionistically provable.


25 
Therefore $\neg P$ is classically provable iff it is intuitionistically


26 
provable.


27 


28 
Proof: Let $Q$ be the conjuction of the propositions $A\vee\neg A$, one for


29 
each atom $A$ in $P$. Now $\neg\neg Q$ is intuitionistically provable because


30 
$\neg\neg(A\vee\neg A)$ is and because doublenegation distributes over


31 
conjunction. If $P$ is provable classically, then clearly $Q\rightarrow P$ is


32 
provable intuitionistically, so $\neg\neg(Q\rightarrow P)$ is also provable


33 
intuitionistically. The latter is intuitionistically equivalent to $\neg\neg


34 
Q\rightarrow\neg\neg P$, hence to $\neg\neg P$, since $\neg\neg Q$ is


35 
intuitionistically provable. Finally, if $P$ is a negation then $\neg\neg P$


36 
is intuitionstically equivalent to $P$. [Andy Pitts] *}


37 


38 
lemma "~~(P&Q) <> ~~P & ~~Q"


39 
by (tactic{*IntPr.fast_tac 1*})


40 


41 
lemma "~~ ((~P > Q) > (~P > ~Q) > P)"


42 
by (tactic{*IntPr.fast_tac 1*})


43 


44 
text{*Doublenegation does NOT distribute over disjunction*}


45 


46 
lemma "~~(P>Q) <> (~~P > ~~Q)"


47 
by (tactic{*IntPr.fast_tac 1*})


48 


49 
lemma "~~~P <> ~P"


50 
by (tactic{*IntPr.fast_tac 1*})


51 


52 
lemma "~~((P > Q  R) > (P>Q)  (P>R))"


53 
by (tactic{*IntPr.fast_tac 1*})


54 


55 
lemma "(P<>Q) <> (Q<>P)"


56 
by (tactic{*IntPr.fast_tac 1*})


57 


58 
lemma "((P > (Q  (Q>R))) > R) > R"


59 
by (tactic{*IntPr.fast_tac 1*})


60 


61 
lemma "(((G>A) > J) > D > E) > (((H>B)>I)>C>J)


62 
> (A>H) > F > G > (((C>B)>I)>D)>(A>C)


63 
> (((F>A)>B) > I) > E"


64 
by (tactic{*IntPr.fast_tac 1*})


65 


66 


67 
text{*Lemmas for the propositional doublenegation translation*}


68 


69 
lemma "P > ~~P"


70 
by (tactic{*IntPr.fast_tac 1*})


71 


72 
lemma "~~(~~P > P)"


73 
by (tactic{*IntPr.fast_tac 1*})


74 


75 
lemma "~~P & ~~(P > Q) > ~~Q"


76 
by (tactic{*IntPr.fast_tac 1*})


77 


78 


79 
text{*The following are classically but not constructively valid.


80 
The attempt to prove them terminates quickly!*}


81 
lemma "((P>Q) > P) > P"


82 
apply (tactic{*IntPr.fast_tac 1*}  )


83 
apply (rule asm_rl) {*Checks that subgoals remain: proof failed.*}


84 
oops


85 


86 
lemma "(P&Q>R) > (P>R)  (Q>R)"


87 
apply (tactic{*IntPr.fast_tac 1*}  )


88 
apply (rule asm_rl) {*Checks that subgoals remain: proof failed.*}


89 
oops


90 


91 


92 
subsection{*de Bruijn formulae*}


93 


94 
text{*de Bruijn formula with three predicates*}


95 
lemma "((P<>Q) > P&Q&R) &


96 
((Q<>R) > P&Q&R) &


97 
((R<>P) > P&Q&R) > P&Q&R"


98 
by (tactic{*IntPr.fast_tac 1*})


99 


100 


101 
text{*de Bruijn formula with five predicates*}


102 
lemma "((P<>Q) > P&Q&R&S&T) &


103 
((Q<>R) > P&Q&R&S&T) &


104 
((R<>S) > P&Q&R&S&T) &


105 
((S<>T) > P&Q&R&S&T) &


106 
((T<>P) > P&Q&R&S&T) > P&Q&R&S&T"


107 
by (tactic{*IntPr.fast_tac 1*})


108 


109 


110 
(*** Problems from of Sahlin, Franzen and Haridi,


111 
An Intuitionistic Predicate Logic Theorem Prover.


112 
J. Logic and Comp. 2 (5), October 1992, 619656.


113 
***)


114 


115 
text{*Problem 1.1*}


116 
lemma "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) <>


117 
(ALL z. EX y. ALL x. p(x) & q(y) & r(z))"


118 
by (tactic{*IntPr.best_dup_tac 1*}) {*SLOW*}


119 


120 
text{*Problem 3.1*}


121 
lemma "~ (EX x. ALL y. mem(y,x) <> ~ mem(x,x))"


122 
by (tactic{*IntPr.fast_tac 1*})


123 


124 
text{*Problem 4.1: hopeless!*}


125 
lemma "(ALL x. p(x) > p(h(x))  p(g(x))) & (EX x. p(x)) & (ALL x. ~p(h(x)))


126 
> (EX x. p(g(g(g(g(g(x)))))))"


127 
oops


128 


129 


130 
subsection{*Intuitionistic FOL: propositional problems based on Pelletier.*}


131 


132 
text{*~~1*}


133 
lemma "~~((P>Q) <> (~Q > ~P))"


134 
by (tactic{*IntPr.fast_tac 1*})


135 


136 
text{*~~2*}


137 
lemma "~~(~~P <> P)"


138 
by (tactic{*IntPr.fast_tac 1*})


139 


140 
text{*3*}


141 
lemma "~(P>Q) > (Q>P)"


142 
by (tactic{*IntPr.fast_tac 1*})


143 


144 
text{*~~4*}


145 
lemma "~~((~P>Q) <> (~Q > P))"


146 
by (tactic{*IntPr.fast_tac 1*})


147 


148 
text{*~~5*}


149 
lemma "~~((PQ>PR) > P(Q>R))"


150 
by (tactic{*IntPr.fast_tac 1*})


151 


152 
text{*~~6*}


153 
lemma "~~(P  ~P)"


154 
by (tactic{*IntPr.fast_tac 1*})


155 


156 
text{*~~7*}


157 
lemma "~~(P  ~~~P)"


158 
by (tactic{*IntPr.fast_tac 1*})


159 


160 
text{*~~8. Peirce's law*}


161 
lemma "~~(((P>Q) > P) > P)"


162 
by (tactic{*IntPr.fast_tac 1*})


163 


164 
text{*9*}


165 
lemma "((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)"


166 
by (tactic{*IntPr.fast_tac 1*})


167 


168 
text{*10*}


169 
lemma "(Q>R) > (R>P&Q) > (P>(QR)) > (P<>Q)"


170 
by (tactic{*IntPr.fast_tac 1*})


171 


172 
subsection{*11. Proved in each direction (incorrectly, says Pelletier!!) *}


173 
lemma "P<>P"


174 
by (tactic{*IntPr.fast_tac 1*})


175 


176 
text{*~~12. Dijkstra's law *}


177 
lemma "~~(((P <> Q) <> R) <> (P <> (Q <> R)))"


178 
by (tactic{*IntPr.fast_tac 1*})


179 


180 
lemma "((P <> Q) <> R) > ~~(P <> (Q <> R))"


181 
by (tactic{*IntPr.fast_tac 1*})


182 


183 
text{*13. Distributive law*}


184 
lemma "P  (Q & R) <> (P  Q) & (P  R)"


185 
by (tactic{*IntPr.fast_tac 1*})


186 


187 
text{*~~14*}


188 
lemma "~~((P <> Q) <> ((Q  ~P) & (~QP)))"


189 
by (tactic{*IntPr.fast_tac 1*})


190 


191 
text{*~~15*}


192 
lemma "~~((P > Q) <> (~P  Q))"


193 
by (tactic{*IntPr.fast_tac 1*})


194 


195 
text{*~~16*}


196 
lemma "~~((P>Q)  (Q>P))"


197 
by (tactic{*IntPr.fast_tac 1*})


198 


199 
text{*~~17*}


200 
lemma "~~(((P & (Q>R))>S) <> ((~P  Q  S) & (~P  ~R  S)))"


201 
by (tactic{*IntPr.fast_tac 1*})


202 


203 
text{*Dijkstra's "Golden Rule"*}


204 
lemma "(P&Q) <> P <> Q <> (PQ)"


205 
by (tactic{*IntPr.fast_tac 1*})


206 


207 


208 
subsection{*****Examples with quantifiers*****}


209 


210 


211 
subsection{*The converse is classical in the following implications...*}


212 


213 
lemma "(EX x. P(x)>Q) > (ALL x. P(x)) > Q"


214 
by (tactic{*IntPr.fast_tac 1*})


215 


216 
lemma "((ALL x. P(x))>Q) > ~ (ALL x. P(x) & ~Q)"


217 
by (tactic{*IntPr.fast_tac 1*})


218 


219 
lemma "((ALL x. ~P(x))>Q) > ~ (ALL x. ~ (P(x)Q))"


220 
by (tactic{*IntPr.fast_tac 1*})


221 


222 
lemma "(ALL x. P(x))  Q > (ALL x. P(x)  Q)"


223 
by (tactic{*IntPr.fast_tac 1*})


224 


225 
lemma "(EX x. P > Q(x)) > (P > (EX x. Q(x)))"


226 
by (tactic{*IntPr.fast_tac 1*})


227 


228 


229 


230 


231 
subsection{*The following are not constructively valid!*}


232 
text{*The attempt to prove them terminates quickly!*}


233 


234 
lemma "((ALL x. P(x))>Q) > (EX x. P(x)>Q)"


235 
apply (tactic{*IntPr.fast_tac 1*}  )


236 
apply (rule asm_rl) {*Checks that subgoals remain: proof failed.*}


237 
oops


238 


239 
lemma "(P > (EX x. Q(x))) > (EX x. P>Q(x))"


240 
apply (tactic{*IntPr.fast_tac 1*}  )


241 
apply (rule asm_rl) {*Checks that subgoals remain: proof failed.*}


242 
oops


243 


244 
lemma "(ALL x. P(x)  Q) > ((ALL x. P(x))  Q)"


245 
apply (tactic{*IntPr.fast_tac 1*}  )


246 
apply (rule asm_rl) {*Checks that subgoals remain: proof failed.*}


247 
oops


248 


249 
lemma "(ALL x. ~~P(x)) > ~~(ALL x. P(x))"


250 
apply (tactic{*IntPr.fast_tac 1*}  )


251 
apply (rule asm_rl) {*Checks that subgoals remain: proof failed.*}


252 
oops


253 


254 
text{*Classically but not intuitionistically valid. Proved by a bug in 1986!*}


255 
lemma "EX x. Q(x) > (ALL x. Q(x))"


256 
apply (tactic{*IntPr.fast_tac 1*}  )


257 
apply (rule asm_rl) {*Checks that subgoals remain: proof failed.*}


258 
oops


259 


260 


261 
subsection{*Hard examples with quantifiers*}


262 


263 
text{*The ones that have not been proved are not known to be valid!


264 
Some will require quantifier duplication  not currently available*}


265 


266 
text{*~~18*}


267 
lemma "~~(EX y. ALL x. P(y)>P(x))"


268 
oops {*NOT PROVED*}


269 


270 
text{*~~19*}


271 
lemma "~~(EX x. ALL y z. (P(y)>Q(z)) > (P(x)>Q(x)))"


272 
oops {*NOT PROVED*}


273 


274 
text{*20*}


275 
lemma "(ALL x y. EX z. ALL w. (P(x)&Q(y)>R(z)&S(w)))


276 
> (EX x y. P(x) & Q(y)) > (EX z. R(z))"


277 
by (tactic{*IntPr.fast_tac 1*})


278 


279 
text{*21*}


280 
lemma "(EX x. P>Q(x)) & (EX x. Q(x)>P) > ~~(EX x. P<>Q(x))"


281 
oops {*NOT PROVED; needs quantifier duplication*}


282 


283 
text{*22*}


284 
lemma "(ALL x. P <> Q(x)) > (P <> (ALL x. Q(x)))"


285 
by (tactic{*IntPr.fast_tac 1*})


286 


287 
text{*~~23*}


288 
lemma "~~ ((ALL x. P  Q(x)) <> (P  (ALL x. Q(x))))"


289 
by (tactic{*IntPr.fast_tac 1*})


290 


291 
text{*24*}


292 
lemma "~(EX x. S(x)&Q(x)) & (ALL x. P(x) > Q(x)R(x)) &


293 
(~(EX x. P(x)) > (EX x. Q(x))) & (ALL x. Q(x)R(x) > S(x))


294 
> ~~(EX x. P(x)&R(x))"


295 
txt{*Not clear why @{text fast_tac}, @{text best_tac}, @{text ASTAR} and


296 
@{text ITER_DEEPEN} all take forever*}


297 
apply (tactic{* IntPr.safe_tac*})


298 
apply (erule impE)


299 
apply (tactic{*IntPr.fast_tac 1*})


300 
by (tactic{*IntPr.fast_tac 1*})


301 


302 
text{*25*}


303 
lemma "(EX x. P(x)) &


304 
(ALL x. L(x) > ~ (M(x) & R(x))) &


305 
(ALL x. P(x) > (M(x) & L(x))) &


306 
((ALL x. P(x)>Q(x))  (EX x. P(x)&R(x)))


307 
> (EX x. Q(x)&P(x))"


308 
by (tactic{*IntPr.fast_tac 1*})


309 


310 
text{*~~26*}


311 
lemma "(~~(EX x. p(x)) <> ~~(EX x. q(x))) &


312 
(ALL x. ALL y. p(x) & q(y) > (r(x) <> s(y)))


313 
> ((ALL x. p(x)>r(x)) <> (ALL x. q(x)>s(x)))"


314 
oops {*NOT PROVED*}


315 


316 
text{*27*}


317 
lemma "(EX x. P(x) & ~Q(x)) &


318 
(ALL x. P(x) > R(x)) &


319 
(ALL x. M(x) & L(x) > P(x)) &


320 
((EX x. R(x) & ~ Q(x)) > (ALL x. L(x) > ~ R(x)))


321 
> (ALL x. M(x) > ~L(x))"


322 
by (tactic{*IntPr.fast_tac 1*})


323 


324 
text{*~~28. AMENDED*}


325 
lemma "(ALL x. P(x) > (ALL x. Q(x))) &


326 
(~~(ALL x. Q(x)R(x)) > (EX x. Q(x)&S(x))) &


327 
(~~(EX x. S(x)) > (ALL x. L(x) > M(x)))


328 
> (ALL x. P(x) & L(x) > M(x))"


329 
by (tactic{*IntPr.fast_tac 1*})


330 


331 
text{*29. Essentially the same as Principia Mathematica *11.71*}


332 
lemma "(EX x. P(x)) & (EX y. Q(y))


333 
> ((ALL x. P(x)>R(x)) & (ALL y. Q(y)>S(y)) <>


334 
(ALL x y. P(x) & Q(y) > R(x) & S(y)))"


335 
by (tactic{*IntPr.fast_tac 1*})


336 


337 
text{*~~30*}


338 
lemma "(ALL x. (P(x)  Q(x)) > ~ R(x)) &


339 
(ALL x. (Q(x) > ~ S(x)) > P(x) & R(x))


340 
> (ALL x. ~~S(x))"


341 
by (tactic{*IntPr.fast_tac 1*})


342 


343 
text{*31*}


344 
lemma "~(EX x. P(x) & (Q(x)  R(x))) &


345 
(EX x. L(x) & P(x)) &


346 
(ALL x. ~ R(x) > M(x))


347 
> (EX x. L(x) & M(x))"


348 
by (tactic{*IntPr.fast_tac 1*})


349 


350 
text{*32*}


351 
lemma "(ALL x. P(x) & (Q(x)R(x))>S(x)) &


352 
(ALL x. S(x) & R(x) > L(x)) &


353 
(ALL x. M(x) > R(x))


354 
> (ALL x. P(x) & M(x) > L(x))"


355 
by (tactic{*IntPr.fast_tac 1*})


356 


357 
text{*~~33*}


358 
lemma "(ALL x. ~~(P(a) & (P(x)>P(b))>P(c))) <>


359 
(ALL x. ~~((~P(a)  P(x)  P(c)) & (~P(a)  ~P(b)  P(c))))"


360 
apply (tactic{*IntPr.best_tac 1*})


361 
done


362 


363 


364 
text{*36*}


365 
lemma "(ALL x. EX y. J(x,y)) &


366 
(ALL x. EX y. G(x,y)) &


367 
(ALL x y. J(x,y)  G(x,y) > (ALL z. J(y,z)  G(y,z) > H(x,z)))


368 
> (ALL x. EX y. H(x,y))"


369 
by (tactic{*IntPr.fast_tac 1*})


370 


371 
text{*37*}


372 
lemma "(ALL z. EX w. ALL x. EX y.


373 
~~(P(x,z)>P(y,w)) & P(y,z) & (P(y,w) > (EX u. Q(u,w)))) &


374 
(ALL x z. ~P(x,z) > (EX y. Q(y,z))) &


375 
(~~(EX x y. Q(x,y)) > (ALL x. R(x,x)))


376 
> ~~(ALL x. EX y. R(x,y))"


377 
oops {*NOT PROVED*}


378 


379 
text{*39*}


380 
lemma "~ (EX x. ALL y. F(y,x) <> ~F(y,y))"


381 
by (tactic{*IntPr.fast_tac 1*})


382 


383 
text{*40. AMENDED*}


384 
lemma "(EX y. ALL x. F(x,y) <> F(x,x)) >


385 
~(ALL x. EX y. ALL z. F(z,y) <> ~ F(z,x))"


386 
by (tactic{*IntPr.fast_tac 1*})


387 


388 
text{*44*}


389 
lemma "(ALL x. f(x) >


390 
(EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) &


391 
(EX x. j(x) & (ALL y. g(y) > h(x,y)))


392 
> (EX x. j(x) & ~f(x))"


393 
by (tactic{*IntPr.fast_tac 1*})


394 


395 
text{*48*}


396 
lemma "(a=b  c=d) & (a=c  b=d) > a=d  b=c"


397 
by (tactic{*IntPr.fast_tac 1*})


398 


399 
text{*51*}


400 
lemma "(EX z w. ALL x y. P(x,y) <> (x=z & y=w)) >


401 
(EX z. ALL x. EX w. (ALL y. P(x,y) <> y=w) <> x=z)"


402 
by (tactic{*IntPr.fast_tac 1*})


403 


404 
text{*52*}


405 
text{*Almost the same as 51. *}


406 
lemma "(EX z w. ALL x y. P(x,y) <> (x=z & y=w)) >


407 
(EX w. ALL y. EX z. (ALL x. P(x,y) <> x=z) <> y=w)"


408 
by (tactic{*IntPr.fast_tac 1*})


409 


410 
text{*56*}


411 
lemma "(ALL x. (EX y. P(y) & x=f(y)) > P(x)) <> (ALL x. P(x) > P(f(x)))"


412 
by (tactic{*IntPr.fast_tac 1*})


413 


414 
text{*57*}


415 
lemma "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &


416 
(ALL x y z. P(x,y) & P(y,z) > P(x,z)) > P(f(a,b), f(a,c))"


417 
by (tactic{*IntPr.fast_tac 1*})


418 


419 
text{*60*}


420 
lemma "ALL x. P(x,f(x)) <> (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))"


421 
by (tactic{*IntPr.fast_tac 1*})


422 


423 
end


424 


425 
