I've been reading through this (https://www.cs.cmu.edu/~fp/courses/15317-f00/handouts/logic....), and have found it way more useful and fun. I expect it's much closer to what the HN crowd would be interested in.
Second of all, it just seems like a mish-mash of like three or four different classes put into one: computability, type theory, first order logic -- all these can be their own concentrations.
Third, it uses type-theoretic terminology ("elimination" and [->e] instead of, e.g., modus ponens [MP]).
Finally, imo that notation really sucks (the top-to-bottom branching is really jarring), I've only seen it used in Type Theory and λ-calculus books.
Some books I suggest: this one from the University of Toronto[1] or this one from one of my favorite classes I took at UCLA[2]. If curious, you can see some problem sets on my website[3].
[1] http://euclid.trentu.ca/math/sb/pcml/pcml-16.pdf
> the top-to-bottom branching is really jarring
What do you mean? From what I've seen from skimming the first few chapters, it uses 100% standard natural deduction proof trees. How would you present the proofs?
(The "linear format" is indeed ugly, but it doesn't seem to be meant for human consumption.)
> I've only seen it used in Type Theory and λ-calculus books
That's the point of the Curry-Howard isomorphism: It's all the same thing. It makes sense to use the same notation.
You're totally right. I just really don't like proof trees, nor do I think they're clear when first starting out studying logic.
FWIW, from the intro:
> However, if you are hoping for help with very elementary logic (e.g. as typically encountered by philosophers in their first-year courses), then let me say straight away that this Guide isn’t designed for you. The only section that directly pertains to this ‘baby logic’ is §1.5; all the rest is about rather more advanced – and eventually very much more advanced – material.
So, he is pretty clear about the guide skipping the first year of foundational material. The title is certainly misleading, however. Maybe
"Teach Yourself Logic Next Year: After spending a year learning basic stuff somewhere else"
would have been better.