4 ms·

At the risk of getting downvoted, I'm just going to say that I really hate this book. First of all, it moves way, way, way too fast. I glossed over it, and chap

by dvt 9y ago

At the risk of getting downvoted, I'm just going to say that I really hate this book. First of all, it moves way, way, way too fast. I glossed over it, and chapter 3 is already the Curry-Howard isomorphism? That took us a semester of λ-calculus to come to grips with. These are big results. 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 http://euclid.trentu.ca/math/sb/pcml/pcml-16.pdf [2] http://www.math.ucla.edu/~dam/135.07w/135notes.pdf http://www.math.ucla.edu/~dam/135.07w/135notes.pdf [3] https://dvt.name/logic https://dvt.name/logic

tom_mellior 9y ago
I have no dog in this race, but... > 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.
- dvt 9y ago
  > I've seen from skimming the first few chapters, it uses 100% standard natural deduction proof trees. How would you present the proofs? 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.
ballenf 9y ago
> First of all, it moves way, way, way too fast. 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.
- sevensor 9y ago
  I believe you and the parent are talking about two different resources. You're referring to to _Teach Yourself Logic in 2017_, but I think the parent is referring to the material from CMU.

by dvt 9y ago

tom_mellior 9y ago

I have no dog in this race, but... > 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.

dvt 9y ago
> I've seen from skimming the first few chapters, it uses 100% standard natural deduction proof trees. How would you present the proofs? 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.

ballenf 9y ago

> First of all, it moves way, way, way too fast. 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.

sevensor 9y ago
I believe you and the parent are talking about two different resources. You're referring to to _Teach Yourself Logic in 2017_, but I think the parent is referring to the material from CMU.