theory s2
imports Main
begin

(* Question 1 *)
lemma a:
  "(\<forall> x. \<forall> y. R x y) = (\<forall> y. \<forall> x. R x y)"
  oops

lemma b:
  "((\<forall> x. P x) \<and> (\<forall> x. Q x)) = (\<forall> x. P x \<and> Q x)"
  oops

lemma c:
  "(\<forall> P. P = True \<or> P = False) \<longrightarrow> (\<forall> P. (\<not> P \<longrightarrow> P) \<longrightarrow> P)"
  oops

lemma d: "(\<forall> P. P = True \<or> P = False) \<longrightarrow> (\<forall> P. (\<not>\<not> P) = P)"
  oops

lemma e:
   "((\<forall>P. \<forall>x. (R x \<and> P x) \<longrightarrow> P (SOME x. P x)) \<and>
     (\<forall> x y. Q x y \<longrightarrow> R y)) 
    \<longrightarrow>
    ((\<forall>x. \<exists>y. Q x y) \<longrightarrow> (\<exists>f. \<forall>x. Q x (f x)))"
  oops

(* Question 2 -- drinker formula *)
(* part (a) *)
lemma df:
  "\<exists> x. D x \<longrightarrow> (\<forall> x. D x)"
  oops

(* part (b) *)


(* Question 3 *)

(* Question 4 *)


end