4 ms·

I've been reading through this (https://www.cs.cmu.edu/~fp/courses/15317-f00/handouts/logic.pdf https://www.cs.cmu.edu/~fp/courses/15317-f00/handouts/logic....)

by imh 9y ago

I've been reading through this (https://www.cs.cmu.edu/~fp/courses/15317-f00/handouts/logic.pdf 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.

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.
fmap 9y ago
It's also much more modern. To be perfectly honest, if you are not doing automated theorem proving you probably never need to know about things like first-order logic or classical logic. Alas, we teach first year students boolean algebra instead of the Brouwer-Heyting-Kolmogoroff interpretation and hopelessly confuse everyone with "paradoxes" before anyone even mentions proof theory...

by imh 9y ago

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.

fmap 9y ago

It's also much more modern. To be perfectly honest, if you are not doing automated theorem proving you probably never need to know about things like first-order logic or classical logic. Alas, we teach first year students boolean algebra instead of the Brouwer-Heyting-Kolmogoroff interpretation and hopelessly confuse everyone with "paradoxes" before anyone even mentions proof theory...