gistfile1.txt

#### First proof I wrote ####
Given ~A & ~B
[ Suppose A | B
  [ Suppose A
    ~A          # By conjunction elimination left with (2)
    F ]         # By negation elimination with (5) and (4)
  [ Suppose B
    ~B          # By conjunction elimination right with (2)
    F ]         # By negation elimination with (8) and (7)
  F ]           # By disjunction elimination with (3), (4-6), (7-9)
~(A | B)        # By negation introduction with (3-10)



#### Better matching the structure given in quiz ####
Given ~A & ~B
~A              # By conjunction elimination left with (16)
~B              # By conjunction elimination right with (16)
[ Suppose A | B
  [ Suppose A
    F ]         # By negation elimination with (17) and (20)
  [ Suppose B
    F ]         # By negation elimination with (18) and (22)
  F ]           # By disjunction elimination with (19), (20-21), (22-23)
~(A | B)        # By negation introduction with (19-24)



#### Even better matching the structure given in quiz ####
Given ~A & ~B
~A              # By conjunction elimination left with (30)
~B              # By conjunction elimination right with (30)
[ Suppose A | B
  [ Suppose A
    F           # By negation elimination with (31) and (34)
    ~(A | B) ]  # By falsehood elimination with (35)
  [ Suppose B
    F           # By negation elimination with (32) and (37)
    ~(A | B) ]  # By falsehood elimination with (38)
  ~(A | B)      # By disjunction elimination (proof by cases) with (33), (34-36), (37-39)
  F ]           # By negation elimination with (40), (33)
~(A | B)        # By negation introduction with (33-41)



Rules for system:
# Implication introduction: from [A ... B], derive A => B
# Implication elimination (modus ponens): from A => B and A, derive B
# Conjunction introduction: from A and B, derive A & B
# Conjunction elimination left: from A & B, derive A
# Conjunction elimination right: from A & B, derive B
# Disjunction introduction left: from A, derive A | B
# Disjunction introduction right: from B, derive A | B
# Disjunction elimination (proof by cases): from A | B, [A ... C], and [B ... C], derive C
# Truth introduction: derive T
# Falsehood elimination: from F, derive A
# Negation introduction: from [A ... F], derive ~A
# Negation elimination: from ~A and A, derive F

Note: it's pretty common to say that negation is just literally A => F.
If you do that, negation introduction/elimination rules are literally
just the implication introduction/elimination rules.

These rules suffice for intuitionstic logic.
There are several interderivable rules for classical logic.
Any *one* of these rules suffices to make the system classical and prove the rest.
# Double negation elimination: from ~~A, derive A
# Proof by contradiction: from [~A ... F], derive A
# Assume the opposite: from [~A ... A], derive A
# Law of the excluded middle: derive ~A | A