% Propositional logic % Author: Brigitte Pientka prop : type. %name prop A. true : prop. false : prop. and : prop -> prop -> prop. %infix right 11 and. imp : prop -> prop -> prop. %infix right 10 imp. or : prop -> prop -> prop. %infix right 11 or. % Intuitionistic, Natural Deduction nd : prop -> type. nd_truei : nd true. nd_falsee : nd false -> nd C. nd_andi : nd A -> nd B -> nd (A and B). nd_andel : nd (A and B) -> nd A. nd_ander : nd (A and B) -> nd B. nd_impi : (nd A -> nd B) -> nd (A imp B). nd_impe : nd (A imp B) -> nd A -> nd B. nd_oril : nd A -> nd (A or B). nd_orir : nd B -> nd (A or B). nd_ore : nd (A or B) -> (nd A -> nd C) -> (nd B -> nd C) -> nd C. % Some example derivations from the homework and class ex1 :nd ((A and B) imp (B and A)) = (nd_impi ([u:nd (A and B)] (nd_andi (nd_ander u) % nd B (nd_andel u)) % nd A ) % nd (B and A) ). ex2 :nd ((A and B) imp B) = (nd_impi ([u:nd (A and B)] (nd_ander u) % nd B ) ). ex3: nd ((A or B) imp (B or A)) = (nd_impi ([u:nd (A or B)] (nd_ore u % nd (A or B) ([v:nd A] nd_orir v) % nd A -> nd (B or A) ([w:nd B] nd_oril w) % nd B -> nd (B or A) ) ) % nd (B or A) ). % nd ((A or B) imp (B or A))