§ 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.