theory a1
imports Main
begin

section "Question 1: Types"

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

section "Question 2: Lambda-Calculus"

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

section "Question 3: Higher Order Unification"

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

section "Question 4: Propositional Logic"

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

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

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

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

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

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

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

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

lemma prop_i:
  "(P \<longrightarrow> Q) = (\<not> (P \<and> \<not> Q))"
  oops

lemma prop_j:
  "(P \<or> \<not> P) \<longrightarrow> (\<not>\<not> P \<longrightarrow> P)"
  oops

lemma prop_k:
  "(P \<or> (Q \<and> R)) \<longrightarrow> ((P \<or> Q) \<and> (P \<or> R))"
  oops

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

end