Theory Classical
section ‹Classical Predicate Calculus Problems›
theory Classical
imports FOL
begin
lemma ‹(P ⟶ Q ∨ R) ⟶ (P ⟶ Q) ∨ (P ⟶ R)›
by blast
subsubsection ‹If and only if›
lemma ‹(P ⟷ Q) ⟷ (Q ⟷ P)›
by blast
lemma ‹¬ (P ⟷ ¬ P)›
by blast
subsection ‹Pelletier's examples›
text ‹
Sample problems from
▪ F. J. Pelletier,
Seventy-Five Problems for Testing Automatic Theorem Provers,
J. Automated Reasoning 2 (1986), 191-216.
Errata, JAR 4 (1988), 236-236.
The hardest problems -- judging by experience with several theorem
provers, including matrix ones -- are 34 and 43.
›
text‹1›
lemma ‹(P ⟶ Q) ⟷ (¬ Q ⟶ ¬ P)›
by blast
text‹2›
lemma ‹¬ ¬ P ⟷ P›
by blast
text‹3›
lemma ‹¬ (P ⟶ Q) ⟶ (Q ⟶ P)›
by blast
text‹4›
lemma ‹(¬ P ⟶ Q) ⟷ (¬ Q ⟶ P)›
by blast
text‹5›
lemma ‹((P ∨ Q) ⟶ (P ∨ R)) ⟶ (P ∨ (Q ⟶ R))›
by blast
text‹6›
lemma ‹P ∨ ¬ P›
by blast
text‹7›
lemma ‹P ∨ ¬ ¬ ¬ P›
by blast
text‹8. Peirce's law›
lemma ‹((P ⟶ Q) ⟶ P) ⟶ P›
by blast
text‹9›
lemma ‹((P ∨ Q) ∧ (¬ P ∨ Q) ∧ (P ∨ ¬ Q)) ⟶ ¬ (¬ P ∨ ¬ Q)›
by blast
text‹10›
lemma ‹(Q ⟶ R) ∧ (R ⟶ P ∧ Q) ∧ (P ⟶ Q ∨ R) ⟶ (P ⟷ Q)›
by blast
text‹11. Proved in each direction (incorrectly, says Pelletier!!)›
lemma ‹P ⟷ P›
by blast
text‹12. "Dijkstra's law"›
lemma ‹((P ⟷ Q) ⟷ R) ⟷ (P ⟷ (Q ⟷ R))›
by blast
text‹13. Distributive law›
lemma ‹P ∨ (Q ∧ R) ⟷ (P ∨ Q) ∧ (P ∨ R)›
by blast
text‹14›
lemma ‹(P ⟷ Q) ⟷ ((Q ∨ ¬ P) ∧ (¬ Q ∨ P))›
by blast
text‹15›
lemma ‹(P ⟶ Q) ⟷ (¬ P ∨ Q)›
by blast
text‹16›
lemma ‹(P ⟶ Q) ∨ (Q ⟶ P)›
by blast
text‹17›
lemma ‹((P ∧ (Q ⟶ R)) ⟶ S) ⟷ ((¬ P ∨ Q ∨ S) ∧ (¬ P ∨ ¬ R ∨ S))›
by blast
subsection ‹Classical Logic: examples with quantifiers›
lemma ‹(∀x. P(x) ∧ Q(x)) ⟷ (∀x. P(x)) ∧ (∀x. Q(x))›
by blast
lemma ‹(∃x. P ⟶ Q(x)) ⟷ (P ⟶ (∃x. Q(x)))›
by blast
lemma ‹(∃x. P(x) ⟶ Q) ⟷ (∀x. P(x)) ⟶ Q›
by blast
lemma ‹(∀x. P(x)) ∨ Q ⟷ (∀x. P(x) ∨ Q)›
by blast
text‹Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
JAR 10 (265-281), 1993. Proof is trivial!›
lemma ‹¬ ((∃x. ¬ P(x)) ∧ ((∃x. P(x)) ∨ (∃x. P(x) ∧ Q(x))) ∧ ¬ (∃x. P(x)))›
by blast
subsection ‹Problems requiring quantifier duplication›
text‹Theorem B of Peter Andrews, Theorem Proving via General Matings,
JACM 28 (1981).›
lemma ‹(∃x. ∀y. P(x) ⟷ P(y)) ⟶ ((∃x. P(x)) ⟷ (∀y. P(y)))›
by blast
text‹Needs multiple instantiation of ALL.›
lemma ‹(∀x. P(x) ⟶ P(f(x))) ∧ P(d) ⟶ P(f(f(f(d))))›
by blast
text‹Needs double instantiation of the quantifier›
lemma ‹∃x. P(x) ⟶ P(a) ∧ P(b)›
by blast
lemma ‹∃z. P(z) ⟶ (∀x. P(x))›
by blast
lemma ‹∃x. (∃y. P(y)) ⟶ P(x)›
by blast
text‹V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23. NOT PROVED.›
lemma
‹∃x x'. ∀y. ∃z z'.
(¬ P(y,y) ∨ P(x,x) ∨ ¬ S(z,x)) ∧
(S(x,y) ∨ ¬ S(y,z) ∨ Q(z',z')) ∧
(Q(x',y) ∨ ¬ Q(y,z') ∨ S(x',x'))›
oops
subsection ‹Hard examples with quantifiers›
text‹18›
lemma ‹∃y. ∀x. P(y) ⟶ P(x)›
by blast
text‹19›
lemma ‹∃x. ∀y z. (P(y) ⟶ Q(z)) ⟶ (P(x) ⟶ Q(x))›
by blast
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 blast
text‹21›
lemma ‹(∃x. P ⟶ Q(x)) ∧ (∃x. Q(x) ⟶ P) ⟶ (∃x. P ⟷ Q(x))›
by blast
text‹22›
lemma ‹(∀x. P ⟷ Q(x)) ⟶ (P ⟷ (∀x. Q(x)))›
by blast
text‹23›
lemma ‹(∀x. P ∨ Q(x)) ⟷ (P ∨ (∀x. Q(x)))›
by blast
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))›
by blast
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 blast
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)))›
by blast
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 blast
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 blast
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 blast
text‹30›
lemma
‹(∀x. P(x) ∨ Q(x) ⟶ ¬ R(x)) ∧
(∀x. (Q(x) ⟶ ¬ S(x)) ⟶ P(x) ∧ R(x))
⟶ (∀x. S(x))›
by blast
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 blast
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 blast
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)))›
by blast
text‹34. AMENDED (TWICE!!). Andrews's challenge.›
lemma
‹((∃x. ∀y. p(x) ⟷ p(y)) ⟷ ((∃x. q(x)) ⟷ (∀y. p(y)))) ⟷
((∃x. ∀y. q(x) ⟷ q(y)) ⟷ ((∃x. p(x)) ⟷ (∀y. q(y))))›
by blast
text‹35›
lemma ‹∃x y. P(x,y) ⟶ (∀u v. P(u,v))›
by blast
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 blast
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))›
by blast
text‹38›
lemma
‹(∀x. p(a) ∧ (p(x) ⟶ (∃y. p(y) ∧ r(x,y))) ⟶
(∃z. ∃w. p(z) ∧ r(x,w) ∧ r(w,z))) ⟷
(∀x. (¬ p(a) ∨ p(x) ∨ (∃z. ∃w. p(z) ∧ r(x,w) ∧ r(w,z))) ∧
(¬ p(a) ∨ ¬ (∃y. p(y) ∧ r(x,y)) ∨
(∃z. ∃w. p(z) ∧ r(x,w) ∧ r(w,z))))›
by blast
text‹39›
lemma ‹¬ (∃x. ∀y. F(y,x) ⟷ ¬ F(y,y))›
by blast
text‹40. AMENDED›
lemma
‹(∃y. ∀x. F(x,y) ⟷ F(x,x)) ⟶
¬ (∀x. ∃y. ∀z. F(z,y) ⟷ ¬ F(z,x))›
by blast
text‹41›
lemma
‹(∀z. ∃y. ∀x. f(x,y) ⟷ f(x,z) ∧ ¬ f(x,x))
⟶ ¬ (∃z. ∀x. f(x,z))›
by blast
text‹42›
lemma ‹¬ (∃y. ∀x. p(x,y) ⟷ ¬ (∃z. p(x,z) ∧ p(z,x)))›
by blast
text‹43›
lemma
‹(∀x. ∀y. q(x,y) ⟷ (∀z. p(z,x) ⟷ p(z,y)))
⟶ (∀x. ∀y. q(x,y) ⟷ q(y,x))›
by blast
text ‹
Other proofs: Can use ‹auto›, which cheats by using rewriting!
‹Deepen_tac› alone requires 253 secs. Or
‹by (mini_tac 1 THEN Deepen_tac 5 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 blast
text‹45›
lemma
‹(∀x. f(x) ∧ (∀y. g(y) ∧ h(x,y) ⟶ j(x,y))
⟶ (∀y. g(y) ∧ h(x,y) ⟶ k(y))) ∧
¬ (∃y. l(y) ∧ k(y)) ∧
(∃x. f(x) ∧ (∀y. h(x,y) ⟶ l(y)) ∧ (∀y. g(y) ∧ h(x,y) ⟶ j(x,y)))
⟶ (∃x. f(x) ∧ ¬ (∃y. g(y) ∧ h(x,y)))›
by blast
text‹46›
lemma
‹(∀x. f(x) ∧ (∀y. f(y) ∧ h(y,x) ⟶ g(y)) ⟶ g(x)) ∧
((∃x. f(x) ∧ ¬ g(x)) ⟶
(∃x. f(x) ∧ ¬ g(x) ∧ (∀y. f(y) ∧ ¬ g(y) ⟶ j(x,y)))) ∧
(∀x y. f(x) ∧ f(y) ∧ h(x,y) ⟶ ¬ j(y,x))
⟶ (∀x. f(x) ⟶ g(x))›
by blast
subsection ‹Problems (mainly) involving equality or functions›
text‹48›
lemma ‹(a = b ∨ c = d) ∧ (a = c ∨ b = d) ⟶ a = d ∨ b = c›
by blast
text‹49. NOT PROVED AUTOMATICALLY. Hard because it involves substitution for
Vars; the type constraint ensures that x,y,z have the same type as a,b,u.›
lemma
‹(∃x y::'a. ∀z. z = x ∨ z = y) ∧ P(a) ∧ P(b) ∧ a ≠ b ⟶ (∀u::'a. P(u))›
apply safe
apply (rule_tac x = ‹a› in allE, assumption)
apply (rule_tac x = ‹b› in allE, assumption)
apply fast
done
text‹50. (What has this to do with equality?)›
lemma ‹(∀x. P(a,x) ∨ (∀y. P(x,y))) ⟶ (∃x. ∀y. P(x,y))›
by blast
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 blast
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 blast
text‹55›
text‹Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
fast DISCOVERS who killed Agatha.›
schematic_goal
‹lives(agatha) ∧ lives(butler) ∧ lives(charles) ∧
(killed(agatha,agatha) ∨ killed(butler,agatha) ∨ killed(charles,agatha)) ∧
(∀x y. killed(x,y) ⟶ hates(x,y) ∧ ¬ richer(x,y)) ∧
(∀x. hates(agatha,x) ⟶ ¬ hates(charles,x)) ∧
(hates(agatha,agatha) ∧ hates(agatha,charles)) ∧
(∀x. lives(x) ∧ ¬ richer(x,agatha) ⟶ hates(butler,x)) ∧
(∀x. hates(agatha,x) ⟶ hates(butler,x)) ∧
(∀x. ¬ hates(x,agatha) ∨ ¬ hates(x,butler) ∨ ¬ hates(x,charles)) ⟶
killed(?who,agatha)›
by fast
text‹56›
lemma ‹(∀x. (∃y. P(y) ∧ x = f(y)) ⟶ P(x)) ⟷ (∀x. P(x) ⟶ P(f(x)))›
by blast
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 blast
text‹58 NOT PROVED AUTOMATICALLY›
lemma ‹(∀x y. f(x) = g(y)) ⟶ (∀x y. f(f(x)) = f(g(y)))›
by (slow elim: subst_context)
text‹59›
lemma ‹(∀x. P(x) ⟷ ¬ P(f(x))) ⟶ (∃x. P(x) ∧ ¬ P(f(x)))›
by blast
text‹60›
lemma ‹∀x. P(x,f(x)) ⟷ (∃y. (∀z. P(z,y) ⟶ P(z,f(x))) ∧ P(x,y))›
by blast
text‹62 as corrected in JAR 18 (1997), page 135›
lemma
‹(∀x. p(a) ∧ (p(x) ⟶ p(f(x))) ⟶ p(f(f(x)))) ⟷
(∀x. (¬ p(a) ∨ p(x) ∨ p(f(f(x)))) ∧
(¬ p(a) ∨ ¬ p(f(x)) ∨ p(f(f(x)))))›
by blast
text ‹From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
fast indeed copes!›
lemma
‹(∀x. F(x) ∧ ¬ G(x) ⟶ (∃y. H(x,y) ∧ J(y))) ∧
(∃x. K(x) ∧ F(x) ∧ (∀y. H(x,y) ⟶ K(y))) ∧
(∀x. K(x) ⟶ ¬ G(x)) ⟶ (∃x. K(x) ∧ J(x))›
by fast
text ‹From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.
It does seem obvious!›
lemma
‹(∀x. F(x) ∧ ¬ G(x) ⟶ (∃y. H(x,y) ∧ J(y))) ∧
(∃x. K(x) ∧ F(x) ∧ (∀y. H(x,y) ⟶ K(y))) ∧
(∀x. K(x) ⟶ ¬ G(x)) ⟶ (∃x. K(x) ⟶ ¬ G(x))›
by fast
text ‹Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
author U. Egly.›
lemma
‹((∃x. A(x) ∧ (∀y. C(y) ⟶ (∀z. D(x,y,z)))) ⟶
(∃w. C(w) ∧ (∀y. C(y) ⟶ (∀z. D(w,y,z)))))
∧
(∀w. C(w) ∧ (∀u. C(u) ⟶ (∀v. D(w,u,v))) ⟶
(∀y z.
(C(y) ∧ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,g)) ∧
(C(y) ∧ ¬ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,b))))
∧
(∀w. C(w) ∧
(∀y z.
(C(y) ∧ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,g)) ∧
(C(y) ∧ ¬ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,b))) ⟶
(∃v. C(v) ∧
(∀y. ((C(y) ∧ Q(w,y,y)) ∧ OO(w,g) ⟶ ¬ P(v,y)) ∧
((C(y) ∧ Q(w,y,y)) ∧ OO(w,b) ⟶ P(v,y) ∧ OO(v,b)))))
⟶ ¬ (∃x. A(x) ∧ (∀y. C(y) ⟶ (∀z. D(x,y,z))))›
by (blast 12)
text ‹
Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1),
p. 105.
›
lemma
‹((∃x. A(x) ∧ (∀y. C(y) ⟶ (∀z. D(x,y,z)))) ⟶
(∃w. C(w) ∧ (∀y. C(y) ⟶ (∀z. D(w,y,z)))))
∧
(∀w. C(w) ∧ (∀u. C(u) ⟶ (∀v. D(w,u,v))) ⟶
(∀y z.
(C(y) ∧ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,g)) ∧
(C(y) ∧ ¬ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,b))))
∧
((∃w. C(w) ∧ (∀y. (C(y) ∧ P(y,y) ⟶ Q(w,y,y) ∧ OO(w,g)) ∧
(C(y) ∧ ¬ P(y,y) ⟶ Q(w,y,y) ∧ OO(w,b))))
⟶
(∃v. C(v) ∧ (∀y. (C(y) ∧ P(y,y) ⟶ P(v,y) ∧ OO(v,g)) ∧
(C(y) ∧ ¬ P(y,y) ⟶ P(v,y) ∧ OO(v,b)))))
⟶
((∃v. C(v) ∧ (∀y. (C(y) ∧ P(y,y) ⟶ P(v,y) ∧ OO(v,g)) ∧
(C(y) ∧ ¬ P(y,y) ⟶ P(v,y) ∧ OO(v,b))))
⟶
(∃u. C(u) ∧ (∀y. (C(y) ∧ P(y,y) ⟶ ¬ P(u,y)) ∧
(C(y) ∧ ¬ P(y,y) ⟶ P(u,y) ∧ OO(u,b)))))
⟶ ¬ (∃x. A(x) ∧ (∀y. C(y) ⟶ (∀z. D(x,y,z))))›
by blast
text ‹Challenge found on info-hol.›
lemma ‹∀x. ∃v w. ∀y z. P(x) ∧ Q(y) ⟶ (P(v) ∨ R(w)) ∧ (R(z) ⟶ Q(v))›
by blast
text ‹
Attributed to Lewis Carroll by S. G. Pulman. The first or last assumption
can be deleted.›
lemma
‹(∀x. honest(x) ∧ industrious(x) ⟶ healthy(x)) ∧
¬ (∃x. grocer(x) ∧ healthy(x)) ∧
(∀x. industrious(x) ∧ grocer(x) ⟶ honest(x)) ∧
(∀x. cyclist(x) ⟶ industrious(x)) ∧
(∀x. ¬ healthy(x) ∧ cyclist(x) ⟶ ¬ honest(x))
⟶ (∀x. grocer(x) ⟶ ¬ cyclist(x))›
by blast
end