(* 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\<open>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]\<close>
lemma\<open>\<not> \<not> (P \<and> Q) \<longleftrightarrow> \<not> \<not> P \<and> \<not> \<not> Q\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
lemma\<open>\<not> \<not> ((\<not> P \<longrightarrow> Q) \<longrightarrow> (\<not> P \<longrightarrow> \<not> Q) \<longrightarrow> P)\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
text\<open>Double-negation does NOT distribute over disjunction.\<close>
lemma\<open>\<not> \<not> (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> \<not> P \<longrightarrow> \<not> \<not> Q)\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
lemma\<open>\<not> \<not> \<not> P \<longleftrightarrow> \<not> P\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
lemma \<open>(((G \<longrightarrow> A) \<longrightarrow> J) \<longrightarrow> D \<longrightarrow> E) \<longrightarrow> (((H \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> C \<longrightarrow> J) \<longrightarrow> (A \<longrightarrow> H) \<longrightarrow> F \<longrightarrow> G \<longrightarrow> (((C \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> D) \<longrightarrow> (A \<longrightarrow> C) \<longrightarrow> (((F \<longrightarrow> A) \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> E\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
text\<open>Admissibility of the excluded middle for negated formulae\<close> lemma\<open>(P \<or> \<not>P \<longrightarrow> \<not>Q) \<longrightarrow> \<not>Q\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
text\<open>The same in a more general form, no ex falso quodlibet\<close> lemma\<open>(P \<or> (P\<longrightarrow>R) \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> Q \<longrightarrow> R\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
subsection \<open>Lemmas for the propositional double-negation translation\<close>
lemma\<open>P \<longrightarrow> \<not> \<not> P\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
lemma\<open>\<not> \<not> (\<not> \<not> P \<longrightarrow> P)\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
lemma\<open>\<not> \<not> P \<and> \<not> \<not> (P \<longrightarrow> Q) \<longrightarrow> \<not> \<not> Q\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
text\<open>The following are classically but not constructively valid.
The attempt to prove them terminates quickly!\<close> lemma\<open>((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P\<close> apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)? apply (rule asm_rl) \<comment> \<open>Checks that subgoals remain: proof failed.\<close> oops
text\<open>de Bruijn formula with three predicates\<close> lemma \<open>((P \<longleftrightarrow> Q) \<longrightarrow> P \<and> Q \<and> R) \<and>
((Q \<longleftrightarrow> R) \<longrightarrow> P \<and> Q \<and> R) \<and>
((R \<longleftrightarrow> P) \<longrightarrow> P \<and> Q \<and> R) \<longrightarrow> P \<and> Q \<and> R\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
text\<open>de Bruijn formula with five predicates\<close> lemma \<open>((P \<longleftrightarrow> Q) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
((Q \<longleftrightarrow> R) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
((R \<longleftrightarrow> S) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
((S \<longleftrightarrow> T) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
((T \<longleftrightarrow> P) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
text\<open>
Problems from of Sahlin, Franzen and Haridi,
An Intuitionistic Predicate Logic Theorem Prover.
J. Logic and Comp. 2 (5), October 1992, 619-656. \<close>
text\<open>Classically but not intuitionistically valid. Proved by a bug in 1986!\<close> lemma\<open>\<exists>x. Q(x) \<longrightarrow> (\<forall>x. Q(x))\<close> apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)? apply (rule asm_rl) \<comment> \<open>Checks that subgoals remain: proof failed.\<close> oops
subsection \<open>Hard examples with quantifiers\<close>
text\<open>
The ones that have not been proved are not known to be valid! Some will
require quantifier duplication -- not currently available. \<close>
text\<open>48\<close> lemma\<open>(a = b \<or> c = d) \<and> (a = c \<or> b = d) \<longrightarrow> a = d \<or> b = c\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
text\<open>51\<close> lemma \<open>(\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
(\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P(x,y) \<longleftrightarrow> y = w) \<longleftrightarrow> x = z)\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
text\<open>52\<close> text\<open>Almost the same as 51.\<close> lemma \<open>(\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
(\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P(x,y) \<longleftrightarrow> x = z) \<longleftrightarrow> y = w)\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
text\<open>56\<close> lemma\<open>(\<forall>x. (\<exists>y. P(y) \<and> x = f(y)) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> P(f(x)))\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
text\<open>57\<close> lemma \<open>P(f(a,b), f(b,c)) \<and> P(f(b,c), f(a,c)) \<and>
(\<forall>x y z. P(x,y) \<and> P(y,z) \<longrightarrow> P(x,z)) \<longrightarrow> P(f(a,b), f(a,c))\<close> by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
