Table of Contents - 20.46.14. Formal methods "surprises"
Prove that some formal expressions using classical logic have meanings that
might not be obvious to some lay readers. I find these are common mistakes
and are worth pointing out to new people. In particular we prove
alimp-surprise, empty-surprise, and eximp-surprise.