# Theory Intuitionistic

theory Intuitionistic
imports IFOL
(*  Title:      FOL/ex/Intuitionistic.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

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 conjuction 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