theory a1
imports Main
begin

section "Question 1: Lambda-Calculus"

text {* submit as part of a .txt or .pdf file *}

section "Question 2: Higher Order Unification"

text {* submit as part of a .txt or .pdf file *}

section "Question 3: Propositional Logic"

lemma prop_a:
"A \<and> B \<longrightarrow> B"
oops

lemma prop_b:
"(P \<or> P) = P"
oops

lemma prop_c:
"\<not>\<not>P \<longrightarrow> P"
oops

lemma prop_d:
"(A \<and> B \<longrightarrow> C) = (A \<longrightarrow> B \<longrightarrow> C)"
oops

lemma prop_e:
"(\<not> x) = (x = False)"
oops

lemma prop_f:
"(a \<longrightarrow> b) = (\<not> (a \<and> \<not> b))"
oops

text {*
Which of the above statements are provable only in a classical logic?
*}

section "Question 4: Higher Order Logic"

lemma hol_a:
"(\<forall>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<forall>x. R x y)"
oops

lemma hol_b:
"(\<exists>x. P x \<and> Q x) \<longrightarrow> ((\<exists>x. P x) \<and> (\<exists>x. Q x))"
oops

lemma hol_c:
"False = (\<forall>P. P)"
oops

lemma hol_d:
"\<exists>R::bool \<Rightarrow> bool \<Rightarrow> bool. ((\<forall>x. \<exists>y. R x y) \<and> \<not>(\<exists>y. \<forall>x. R x y))"
oops

lemma hol_e:
"(\<forall>x. \<not> (R x) \<longrightarrow> RM x) \<Longrightarrow> (\<forall>x. \<not> RM x \<longrightarrow> R x)"
oops

lemma hol_f:
"\<lbrakk>(\<forall>x. \<not> (R x) \<longrightarrow> R (M x)); (\<exists>x. R x)\<rbrakk> \<Longrightarrow> (\<exists>x. R x \<and> R (M (M x)))"
oops

text {*
Formalise and prove the following statement using only the proof methods and rules as earlier in this question.

If every poor person has a rich mother, then there is a rich person
with a rich grandmother.
*}

lemma rich_grandmothers:
"formalise_the_statement_here"
oops

end