§ You could have invented Sequents
 Key idea: define a notation called
Γ => Δ
iff the conjunction of sentences in gamma implies the disjunction of terms in delta.  Why would anybody do this? isn't this weird?
 It's because we first note what we need to think about consequence, validity, and unsatisfiability.

d1
is a consequence of Γ
iff g1 /\ g2 .. /\ gn => d1

d1
is valid iff empty => d1
, or written differently, 0 => {d1}
. 
Γ
is unsatisfiable iff g1 /\ ... /\ gn => False
, or written differently, Γ => 0
 Thus, see that on the RHS, we need a set with 0 or 1 inhabitant. We can think of this as
Maybe
, smooshed together with \/
, since we want the empty set to represent False
.  Recall that haskell teaches us to replace failure with a list of successes!
 Thus we should use
Γ => Δ
where on the RHS, we have a list that is smooshed together by or ( \/
)!  Great, we have successfully invented sequents.