header {* Pr\"adikatenlogik *}

(*<*)
theory PL = Main:
(*>*)

text {* Beweisen Sie die folgenden Formeln der Pr\"adikatenlogik mit den 
Regeln des nat\"urlichen Schlie{\ss}ens wie auf Blatt 4.
*}

lemma "\<exists>x. (P x \<longrightarrow> (\<forall>x. P x))" oops
lemma "(\<exists>x. \<forall>y. P x y) \<longrightarrow> (\<forall>y. \<exists>x. P x y)" oops
lemma "(\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)" oops
lemma "\<forall>x. P x \<longrightarrow> Q (f x) \<Longrightarrow> \<exists>x. P x \<Longrightarrow> \<exists>x. Q (f x)" oops

text{*
Zus\"atzlich zu den Regeln der Aussagenlogik k\"onnen Sie die folgenden 
Regeln verwenden:\\
@{text "exI:"}~@{thm exI[no_vars]},\\
@{text "exE:"}~@{thm exE[no_vars]},\\
@{text "allI:"}~@{thm allI[no_vars]},\\ 
@{text "allE:"}~@{thm allE[no_vars]}.\\
*}

(*<*)
end
(*>*)