technical note
§ You Could Have Invented Sequents
created 2022-08-22
- 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.
❦