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: Propositional Logic"

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

lemma prop_c:
  "(P \<or> P) = 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> A) = Q \<Longrightarrow> Q \<or> B"
  oops
    
lemma prop_g:
  "(a \<longrightarrow> b) = (\<not> (a \<and> \<not> b))"
  oops

lemma prop_h:
  "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
  oops

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

text {* Do not use cases, classical, or ccontr for proj_j: *}
lemma prop_j:
  "\<not> (\<not> (\<not> P \<or> Q) \<or> P) \<or> P \<Longrightarrow> P \<or> \<not> P"
  oops

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

end