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:
  "B \<longrightarrow> (B \<or> A)"
  oops

lemma prop_b:
  "(A = True) = A"
  oops

lemma prop_c:
  "(A = False) = (\<not> A)"
  oops

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

lemma prop_e: "\<not>\<not>P \<longrightarrow> P"
  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. P x) \<or> (\<forall>x. Q x) \<longrightarrow> (\<forall>x. P x \<or> Q x)"
  oops

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

lemma hol_c:
  "(\<forall>x. Q x = P x) \<and> ((\<exists>x. P x) \<longrightarrow> C) \<and> (\<exists>x. Q x) \<longrightarrow> C"
  oops

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

lemma hol_e:
  "\<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 "formalise_the_statement_here"
  oops

end