Theory Intuitionistic
section ‹Intuitionistic First-Order Logic›
theory Intuitionistic
imports IFOL
begin
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›)
text ‹Admissibility of the excluded middle for negated formulae›
lemma ‹(P ∨ ¬P ⟶ ¬Q) ⟶ ¬Q›
by (tactic ‹IntPr.fast_tac \<^context> 1›)
text ‹The same in a more general form, no ex falso quodlibet›
lemma ‹(P ∨ (P⟶R) ⟶ Q ⟶ R) ⟶ Q ⟶ R›
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)
oops
lemma ‹(P ∧ Q ⟶ R) ⟶ (P ⟶ R) ∨ (Q ⟶ R)›
apply (tactic ‹IntPr.fast_tac \<^context> 1›)?
apply (rule asm_rl)
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›)
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)
oops
lemma ‹(P ⟶ (∃x. Q(x))) ⟶ (∃x. P ⟶ Q(x))›
apply (tactic ‹IntPr.fast_tac \<^context> 1›)?
apply (rule asm_rl)
oops
lemma ‹(∀x. P(x) ∨ Q) ⟶ ((∀x. P(x)) ∨ Q)›
apply (tactic ‹IntPr.fast_tac \<^context> 1›)?
apply (rule asm_rl)
oops
lemma ‹(∀x. ¬ ¬ P(x)) ⟶ ¬ ¬ (∀x. P(x))›
apply (tactic ‹IntPr.fast_tac \<^context> 1›)?
apply (rule asm_rl)
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)
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
text‹‹¬¬›19›
lemma ‹¬ ¬ (∃x. ∀y z. (P(y) ⟶ Q(z)) ⟶ (P(x) ⟶ Q(x)))›
oops
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
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
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
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