(* Title: FOL/ex/Intuitionistic.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge *) section \Intuitionistic First-Order Logic\ theory Intuitionistic imports IFOL begin (* Single-step ML commands: by (IntPr.step_tac 1) by (biresolve_tac safe_brls 1); by (biresolve_tac haz_brls 1); by (assume_tac 1); by (IntPr.safe_tac 1); by (IntPr.mp_tac 1); by (IntPr.fast_tac @{context} 1); *) text\Metatheorem (for \emph{propositional} formulae): $P$ is classically provable iff $\neg\neg P$ is intuitionistically provable. Therefore $\neg P$ is classically provable iff it is intuitionistically provable. Proof: Let $Q$ be the conjunction of the propositions $A\vee\neg A$, one for each atom $A$ in $P$. Now $\neg\neg Q$ is intuitionistically provable because $\neg\neg(A\vee\neg A)$ is and because double-negation distributes over conjunction. If $P$ is provable classically, then clearly $Q\rightarrow P$ is provable intuitionistically, so $\neg\neg(Q\rightarrow P)$ is also provable intuitionistically. The latter is intuitionistically equivalent to $\neg\neg Q\rightarrow\neg\neg P$, hence to $\neg\neg P$, since $\neg\neg Q$ is intuitionistically provable. Finally, if $P$ is a negation then $\neg\neg P$ is intuitionstically equivalent to $P$. [Andy Pitts]\ lemma \\ \ (P \ Q) \ \ \ P \ \ \ Q\ by (tactic \IntPr.fast_tac @{context} 1\) lemma \\ \ ((\ P \ Q) \ (\ P \ \ Q) \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) text \Double-negation does NOT distribute over disjunction.\ lemma \\ \ (P \ Q) \ (\ \ P \ \ \ Q)\ by (tactic \IntPr.fast_tac @{context} 1\) lemma \\ \ \ P \ \ P\ by (tactic \IntPr.fast_tac @{context} 1\) lemma \\ \ ((P \ Q \ R) \ (P \ Q) \ (P \ R))\ by (tactic \IntPr.fast_tac @{context} 1\) lemma \(P \ Q) \ (Q \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) lemma \((P \ (Q \ (Q \ R))) \ R) \ R\ by (tactic \IntPr.fast_tac @{context} 1\) lemma \(((G \ A) \ J) \ D \ E) \ (((H \ B) \ I) \ C \ J) \ (A \ H) \ F \ G \ (((C \ B) \ I) \ D) \ (A \ C) \ (((F \ A) \ B) \ I) \ E\ by (tactic \IntPr.fast_tac @{context} 1\) subsection \Lemmas for the propositional double-negation translation\ lemma \P \ \ \ P\ by (tactic \IntPr.fast_tac @{context} 1\) lemma \\ \ (\ \ P \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) lemma \\ \ P \ \ \ (P \ Q) \ \ \ Q\ by (tactic \IntPr.fast_tac @{context} 1\) text \The following are classically but not constructively valid. The attempt to prove them terminates quickly!\ lemma \((P \ Q) \ P) \ P\ apply (tactic \IntPr.fast_tac @{context} 1\)? apply (rule asm_rl) \ \Checks that subgoals remain: proof failed.\ oops lemma \(P \ Q \ R) \ (P \ R) \ (Q \ R)\ apply (tactic \IntPr.fast_tac @{context} 1\)? apply (rule asm_rl) \ \Checks that subgoals remain: proof failed.\ oops subsection \de Bruijn formulae\ text \de Bruijn formula with three predicates\ lemma \((P \ Q) \ P \ Q \ R) \ ((Q \ R) \ P \ Q \ R) \ ((R \ P) \ P \ Q \ R) \ P \ Q \ R\ by (tactic \IntPr.fast_tac @{context} 1\) text \de Bruijn formula with five predicates\ lemma \((P \ Q) \ P \ Q \ R \ S \ T) \ ((Q \ R) \ P \ Q \ R \ S \ T) \ ((R \ S) \ P \ Q \ R \ S \ T) \ ((S \ T) \ P \ Q \ R \ S \ T) \ ((T \ P) \ P \ Q \ R \ S \ T) \ P \ Q \ R \ S \ T\ by (tactic \IntPr.fast_tac @{context} 1\) text \ Problems from of Sahlin, Franzen and Haridi, An Intuitionistic Predicate Logic Theorem Prover. J. Logic and Comp. 2 (5), October 1992, 619-656. \ text\Problem 1.1\ lemma \(\x. \y. \z. p(x) \ q(y) \ r(z)) \ (\z. \y. \x. p(x) \ q(y) \ r(z))\ by (tactic \IntPr.best_dup_tac @{context} 1\) \ \SLOW\ text\Problem 3.1\ lemma \\ (\x. \y. mem(y,x) \ \ mem(x,x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\Problem 4.1: hopeless!\ lemma \(\x. p(x) \ p(h(x)) \ p(g(x))) \ (\x. p(x)) \ (\x. \ p(h(x))) \ (\x. p(g(g(g(g(g(x)))))))\ oops subsection \Intuitionistic FOL: propositional problems based on Pelletier.\ text\\\\\1\ lemma \\ \ ((P \ Q) \ (\ Q \ \ P))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\2\ lemma \\ \ (\ \ P \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) text\3\ lemma \\ (P \ Q) \ (Q \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\4\ lemma \\ \ ((\ P \ Q) \ (\ Q \ P))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\5\ lemma \\ \ ((P \ Q \ P \ R) \ P \ (Q \ R))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\6\ lemma \\ \ (P \ \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\7\ lemma \\ \ (P \ \ \ \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\8. Peirce's law\ lemma \\ \ (((P \ Q) \ P) \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) text\9\ lemma \((P \ Q) \ (\ P \ Q) \ (P \ \ Q)) \ \ (\ P \ \ Q)\ by (tactic \IntPr.fast_tac @{context} 1\) text\10\ lemma \(Q \ R) \ (R \ P \ Q) \ (P \ (Q \ R)) \ (P \ Q)\ by (tactic \IntPr.fast_tac @{context} 1\) subsection\11. Proved in each direction (incorrectly, says Pelletier!!)\ lemma \P \ P\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\12. Dijkstra's law\ lemma \\ \ (((P \ Q) \ R) \ (P \ (Q \ R)))\ by (tactic \IntPr.fast_tac @{context} 1\) lemma \((P \ Q) \ R) \ \ \ (P \ (Q \ R))\ by (tactic \IntPr.fast_tac @{context} 1\) text\13. Distributive law\ lemma \P \ (Q \ R) \ (P \ Q) \ (P \ R)\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\14\ lemma \\ \ ((P \ Q) \ ((Q \ \ P) \ (\ Q \ P)))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\15\ lemma \\ \ ((P \ Q) \ (\ P \ Q))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\16\ lemma \\ \ ((P \ Q) \ (Q \ P))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\17\ lemma \\ \ (((P \ (Q \ R)) \ S) \ ((\ P \ Q \ S) \ (\ P \ \ R \ S)))\ by (tactic \IntPr.fast_tac @{context} 1\) text \Dijkstra's ``Golden Rule''\ lemma \(P \ Q) \ P \ Q \ (P \ Q)\ by (tactic \IntPr.fast_tac @{context} 1\) section \Examples with quantifiers\ subsection \The converse is classical in the following implications \dots\ lemma \(\x. P(x) \ Q) \ (\x. P(x)) \ Q\ by (tactic \IntPr.fast_tac @{context} 1\) lemma \((\x. P(x)) \ Q) \ \ (\x. P(x) \ \ Q)\ by (tactic \IntPr.fast_tac @{context} 1\) lemma \((\x. \ P(x)) \ Q) \ \ (\x. \ (P(x) \ Q))\ by (tactic \IntPr.fast_tac @{context} 1\) lemma \(\x. P(x)) \ Q \ (\x. P(x) \ Q)\ by (tactic \IntPr.fast_tac @{context} 1\) lemma \(\x. P \ Q(x)) \ (P \ (\x. Q(x)))\ by (tactic \IntPr.fast_tac @{context} 1\) subsection \The following are not constructively valid!\ text \The attempt to prove them terminates quickly!\ lemma \((\x. P(x)) \ Q) \ (\x. P(x) \ Q)\ apply (tactic \IntPr.fast_tac @{context} 1\)? apply (rule asm_rl) \ \Checks that subgoals remain: proof failed.\ oops lemma \(P \ (\x. Q(x))) \ (\x. P \ Q(x))\ apply (tactic \IntPr.fast_tac @{context} 1\)? apply (rule asm_rl) \ \Checks that subgoals remain: proof failed.\ oops lemma \(\x. P(x) \ Q) \ ((\x. P(x)) \ Q)\ apply (tactic \IntPr.fast_tac @{context} 1\)? apply (rule asm_rl) \ \Checks that subgoals remain: proof failed.\ oops lemma \(\x. \ \ P(x)) \ \ \ (\x. P(x))\ apply (tactic \IntPr.fast_tac @{context} 1\)? apply (rule asm_rl) \ \Checks that subgoals remain: proof failed.\ oops text \Classically but not intuitionistically valid. Proved by a bug in 1986!\ lemma \\x. Q(x) \ (\x. Q(x))\ apply (tactic \IntPr.fast_tac @{context} 1\)? apply (rule asm_rl) \ \Checks that subgoals remain: proof failed.\ oops subsection \Hard examples with quantifiers\ text \ The ones that have not been proved are not known to be valid! Some will require quantifier duplication -- not currently available. \ text\\\\\18\ lemma \\ \ (\y. \x. P(y) \ P(x))\ oops \ \NOT PROVED\ text\\\\\19\ lemma \\ \ (\x. \y z. (P(y) \ Q(z)) \ (P(x) \ Q(x)))\ oops \ \NOT PROVED\ text\20\ lemma \(\x y. \z. \w. (P(x) \ Q(y) \ R(z) \ S(w))) \ (\x y. P(x) \ Q(y)) \ (\z. R(z))\ by (tactic \IntPr.fast_tac @{context} 1\) text\21\ lemma \(\x. P \ Q(x)) \ (\x. Q(x) \ P) \ \ \ (\x. P \ Q(x))\ oops \ \NOT PROVED; needs quantifier duplication\ text\22\ lemma \(\x. P \ Q(x)) \ (P \ (\x. Q(x)))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\23\ lemma \\ \ ((\x. P \ Q(x)) \ (P \ (\x. Q(x))))\ by (tactic \IntPr.fast_tac @{context} 1\) text\24\ lemma \\ (\x. S(x) \ Q(x)) \ (\x. P(x) \ Q(x) \ R(x)) \ (\ (\x. P(x)) \ (\x. Q(x))) \ (\x. Q(x) \ R(x) \ S(x)) \ \ \ (\x. P(x) \ R(x))\ text \ Not clear why \fast_tac\, \best_tac\, \ASTAR\ and \ITER_DEEPEN\ all take forever. \ apply (tactic \IntPr.safe_tac @{context}\) apply (erule impE) apply (tactic \IntPr.fast_tac @{context} 1\) apply (tactic \IntPr.fast_tac @{context} 1\) done text\25\ lemma \(\x. P(x)) \ (\x. L(x) \ \ (M(x) \ R(x))) \ (\x. P(x) \ (M(x) \ L(x))) \ ((\x. P(x) \ Q(x)) \ (\x. P(x) \ R(x))) \ (\x. Q(x) \ P(x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\26\ lemma \(\ \ (\x. p(x)) \ \ \ (\x. q(x))) \ (\x. \y. p(x) \ q(y) \ (r(x) \ s(y))) \ ((\x. p(x) \ r(x)) \ (\x. q(x) \ s(x)))\ oops \ \NOT PROVED\ text\27\ lemma \(\x. P(x) \ \ Q(x)) \ (\x. P(x) \ R(x)) \ (\x. M(x) \ L(x) \ P(x)) \ ((\x. R(x) \ \ Q(x)) \ (\x. L(x) \ \ R(x))) \ (\x. M(x) \ \ L(x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\28. AMENDED\ lemma \(\x. P(x) \ (\x. Q(x))) \ (\ \ (\x. Q(x) \ R(x)) \ (\x. Q(x) \ S(x))) \ (\ \ (\x. S(x)) \ (\x. L(x) \ M(x))) \ (\x. P(x) \ L(x) \ M(x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\29. Essentially the same as Principia Mathematica *11.71\ lemma \(\x. P(x)) \ (\y. Q(y)) \ ((\x. P(x) \ R(x)) \ (\y. Q(y) \ S(y)) \ (\x y. P(x) \ Q(y) \ R(x) \ S(y)))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\30\ lemma \(\x. (P(x) \ Q(x)) \ \ R(x)) \ (\x. (Q(x) \ \ S(x)) \ P(x) \ R(x)) \ (\x. \ \ S(x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\31\ lemma \\ (\x. P(x) \ (Q(x) \ R(x))) \ (\x. L(x) \ P(x)) \ (\x. \ R(x) \ M(x)) \ (\x. L(x) \ M(x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\32\ lemma \(\x. P(x) \ (Q(x) \ R(x)) \ S(x)) \ (\x. S(x) \ R(x) \ L(x)) \ (\x. M(x) \ R(x)) \ (\x. P(x) \ M(x) \ L(x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\33\ lemma \(\x. \ \ (P(a) \ (P(x) \ P(b)) \ P(c))) \ (\x. \ \ ((\ P(a) \ P(x) \ P(c)) \ (\ P(a) \ \ P(b) \ P(c))))\ apply (tactic \IntPr.best_tac @{context} 1\) done text\36\ lemma \(\x. \y. J(x,y)) \ (\x. \y. G(x,y)) \ (\x y. J(x,y) \ G(x,y) \ (\z. J(y,z) \ G(y,z) \ H(x,z))) \ (\x. \y. H(x,y))\ by (tactic \IntPr.fast_tac @{context} 1\) text\37\ lemma \(\z. \w. \x. \y. \ \ (P(x,z) \ P(y,w)) \ P(y,z) \ (P(y,w) \ (\u. Q(u,w)))) \ (\x z. \ P(x,z) \ (\y. Q(y,z))) \ (\ \ (\x y. Q(x,y)) \ (\x. R(x,x))) \ \ \ (\x. \y. R(x,y))\ oops \ \NOT PROVED\ text\39\ lemma \\ (\x. \y. F(y,x) \ \ F(y,y))\ by (tactic \IntPr.fast_tac @{context} 1\) text\40. AMENDED\ lemma \(\y. \x. F(x,y) \ F(x,x)) \ \ (\x. \y. \z. F(z,y) \ \ F(z,x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\44\ lemma \(\x. f(x) \ (\y. g(y) \ h(x,y) \ (\y. g(y) \ \ h(x,y)))) \ (\x. j(x) \ (\y. g(y) \ h(x,y))) \ (\x. j(x) \ \ f(x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\48\ lemma \(a = b \ c = d) \ (a = c \ b = d) \ a = d \ b = c\ by (tactic \IntPr.fast_tac @{context} 1\) text\51\ lemma \(\z w. \x y. P(x,y) \ (x = z \ y = w)) \ (\z. \x. \w. (\y. P(x,y) \ y = w) \ x = z)\ by (tactic \IntPr.fast_tac @{context} 1\) text\52\ text \Almost the same as 51.\ lemma \(\z w. \x y. P(x,y) \ (x = z \ y = w)) \ (\w. \y. \z. (\x. P(x,y) \ x = z) \ y = w)\ by (tactic \IntPr.fast_tac @{context} 1\) text\56\ lemma \(\x. (\y. P(y) \ x = f(y)) \ P(x)) \ (\x. P(x) \ P(f(x)))\ by (tactic \IntPr.fast_tac @{context} 1\) text\57\ lemma \P(f(a,b), f(b,c)) \ P(f(b,c), f(a,c)) \ (\x y z. P(x,y) \ P(y,z) \ P(x,z)) \ P(f(a,b), f(a,c))\ by (tactic \IntPr.fast_tac @{context} 1\) text\60\ lemma \\x. P(x,f(x)) \ (\y. (\z. P(z,y) \ P(z,f(x))) \ P(x,y))\ by (tactic \IntPr.fast_tac @{context} 1\) end