9 ms·

Teach Yourself Logic: A Study Guide [pdf]

392 points by furcyd 8y ago

pmoriarty 8y ago
I'd like to recommend Logic 2010[1], a application with which you can do logic exercises to learn the natural deduction system from *"Logic: Techniques of Formal Reasoning" by Kalish, Montague, and Mar.[2] The program is officially only for MacOS and Windows, but with a little work it's possible to get it running on Linux, as it's just Java. The exercises are fun, and the program will not only check your work to make sure it's right, but also point out where and sometimes why it's wrong. [1] - https://logiclx.humnet.ucla.edu/Logic/Download https://logiclx.humnet.ucla.edu/Logic/Download [2] - https://www.amazon.com/Logic-Techniques-Reasoning-Donald-Kalish/dp/0195155041 https://www.amazon.com/Logic-Techniques-Reasoning-Donald-Kal...
- cortesoft 8y ago
  Oh man, brings back memories. I used an earlier version of this program as a philosophy undergrad at UCLA in the early 2000s. I LOVED doing the homework in my logic classes!
- nixpulvis 8y ago
  I'm assuming that program is more approachable than something like Coq or others? I used ACL2 a bit in college, and could imagine people being frustrated trying to learn it on their own.
  - pvarangot 8y ago
    It's infinitely more approachable than Coq/PVS or whatever other theorem prover since it was designed for teaching and not a research tool or potential application to actually verifying properties of complex systems.
nixpulvis 8y ago
I've been working my way through Kleene's "Mathmatical Logic". It's a great read so far, touching on the details and proofs in some detail. I'm looking forward to the chapters on completeness and the like. I was mostly inspired to get his book because of the Kleene star, who knows why. Also, though very different, I just got GEB for Christmas, so I guess I'll be reading that finally now too.
dang 8y ago
2017: https://news.ycombinator.com/item?id=15114139 https://news.ycombinator.com/item?id=15114139 2015: https://news.ycombinator.com/item?id=10819702 https://news.ycombinator.com/item?id=10819702
- nixpulvis 8y ago
  Off topic: I'm honestly kinda surprised this kind of comment isn't built into HN by this point. There's often so many good comments from old articles we rely on adventurous users to dig up.
  - barry-cotter 8y ago
    It is. Ctrl + F “past” and you’ll see it between hide and web up top.
BucketSort 8y ago
Fyi, there are many correspondences between logic and type theory / functional programming. I have found that as a programmer, many ideas are more accessible to me in type theory as opposed to logic. Languages like Haskell are great for exploring these relationships. This is also known as computational trinitarianism - https://ncatlab.org/nlab/show/computational+trinitarianism https://ncatlab.org/nlab/show/computational+trinitarianism Robert Harper, the computer scientist that coined "computational trinitarianism," has a series of lectures on the foundations of type theory including some commentary on these correspondences - https://youtu.be/9SnefrwBIDc https://youtu.be/9SnefrwBIDc.
- _emacsomancer_ 8y ago
  > many ideas are more accessible to me in type theory as opposed to logic But how do you understand type theory without some basic understanding of logic?
  - BucketSort 8y ago
    It's possible, but I guess I should have specified "logic outside the standard curriculum of computer science studies." For example, I think understanding bits of modal logic through how monads behave is much more fruitful for a CS person. Also, I want to further add here that the correspondence between proofs and programs is known as the Curry–Howard correspondence. This is the more general term under which these relationships between type theory and logic are discussed. The term "computational trinitarianism" also adds a further correspondence to categories. ( As shown in my link above ).
    - BucketSort 8y ago
      Also, "Curry–Howard–Lambek correspondence" is the real name for "computational trinitarianism." I like the latter better because I don't like naming mathematical things after people, which have no bearing on the actual meaning.
    - _emacsomancer_ 8y ago
      Ok, but students need to understand at least ¬, ∧, ∨, →, and there are other useful equivalencies as between sets and (characteristic) functions etc.
olooney 8y ago
This guide covers many different topics and specialties related to logic so it may help to introduce a taxonomy so we don't get intimidated by the breadth of Dr. Smith's scholarship. Let's break it down into 5 topics: 1. Using a well-known and widely accepted system of logic to produce proofs and solve problems. A working man's logic is propositional logic (AND, OR, NOT, and the material conditional) plus first-order predicate logic (quantifiers "there exits" and "for all" over bound variables), natural deduction, and ZFC set theory. 2. "non-standard" logic systems which are somehow "better" or "more expressive:" 2nd order logics, modal logics, many-valued logics, etc. 3. Meta-mathematical investigations into the properties of different formal logic systems: model theory, proof theory, forcing, consistency, completeness, etc. 4. The philosophy of logic: Semantics, sense/reference, truth, nominalism/realism, theory of descriptions, etc. 5. Logic and computability: lambda calculus, recursive functions, turing machines, complexity classes, etc. This is somewhat tangential to logic proper but there are connections and Dr. Smith has a section on it so it's worth enumerating. While everyone will need to know (1) as a working man's logic, the other topics are more or less independent and can be approached independently. For people just starting out and finding this study guide pretty overwhelming, let me re-emphasize two of Dr. Smith's suggestions for starting points: Smullyan's First Order Logic and Halmos's Naive Set Theory. These two books will get you to the same depth of understanding that 95% of working mathematicians need or apply in their day-to-day work, and it's a fact that 95% of modern mathematical theories are built on (formalized within) ZFC set theory and first order logic. https://en.wikipedia.org/wiki/Naive_Set_Theory_(book) https://en.wikipedia.org/wiki/Naive_Set_Theory_(book) http://store.doverpublications.com/0486683702.html http://store.doverpublications.com/0486683702.html I also suggest the online game The Incredible Proof Machine. It's extremely helpful to have a computer formally check your proofs when you're just starting out in logic because it's incredibly easy to "cheat" and skip steps or use rules that "make sense" but aren't part of the formal system your using. TIPM lets you do that without learning any specialized syntax. http://incredible.pm/ http://incredible.pm/
topynate 8y ago
I've been following this guide for several months. It's made some excellent recommendations so far. Prospective type theorists, students of linear logic, etc. will have to venture beyond the reading list, but having a good grasp of the modern fundamentals of logic has made a big difference to me in how well I can follow texts like HoTT.
jesuslop 8y ago
And for leisure, www.logicomix.com (a surprising graphical novel bio-"pic" of Russell and some episodes of the foundations saga).
edoo 8y ago
Studying logic taught me one of the more important distinctions in life is identifying when things are always true vs sometimes true. We are taught to often group things that are mostly true into the always true category. This is effectively lossy compression that can introduce serious error into your line of reasoning.
- nurettin 8y ago
  That doesn't make sense to me as in real life most of our reasoning comes from syllogisms for practical reasons. And if something is consistently demonstrated to be true, chances are it will continue to be so, so we take our chances with that. It isn't lossy anything, it is life.
  - claudiawerner 8y ago
    As a side note, it's always kind of funny to see hackers/computer types try and frame discussions in terms of things which are familiar to them, and these comments are often highly upvoted because of the explanation. In this instance, "lossy compression". But few people ever seem to question whether the domain of such categorisations is at all applicable to real human situations, and even if it's possible to make such categorisations. Is the method of the natural sciences or mathematics applicable identically to the social sciences? Often hackers assume this to be the case. I think there's also an element that hackers want to feel as though using the concepts they've developed which are very powerful in computer science should therefore be key to understanding the world as a whole. It's partially being eager to apply one's knowledge and partly hubris and unwillingness to defer to philosophy, sociology or critical theory which they view as less rigorous (and therefore bad).
    - hnuser1234 8y ago
      Why is it funny that people understand things in terms of their experience? The original comment about "lossy compression" essentially stated that humans don't have perfect thinking/memory/processing of probabilities. Do you disagree? Does it matter whether or not the wording of this idea uses computer science terms? Sure, technical people might try to apply methods from technical disciplines to social ones. Sometimes it works, sometimes it doesn't. As a rule, however, I don't think anyone assumes mathematics will completely replace social studies. We might use statistics to better understand social studies, but the social context is still distinctive from pure math, and always will be. Some of the best hackers are the ones who DO borrow ideas from other disciplines. And all other disciplines can often benefit from applying increasingly complex statistical methods, aided by computer and data scientists.
alphakilo 8y ago
On pages 43-44, the author mentions a member of my school's faculty G. Toualakis. The criticisms are valid and his textbook is convoluted. I appreciate the recognition on unnecessary formalism and complexity. For a 1000 level logic course that Software Engineers, Computer Engineers and Computer Science must take, it is extreme. Overall, interesting to see!
- bsznjyewgd 8y ago
  The author is refering to a different Tourlakis text than the one used in the 1000 level logic course for compsci students.
james_s_tayler 8y ago
This is a pretty epic map. Does anyone know of any others for other domains of knowledge??
khrm 8y ago
A much shorter guide by the same author in 2 pages instead of 90: https://www.logicmatters.net/tyl/shorter-tyl/ https://www.logicmatters.net/tyl/shorter-tyl/
bostonvaulter2 8y ago
Is there an ePub version of the guide available anywhere?

392 points by furcyd 8y ago

I'd like to recommend Logic 2010[1], a application with which you can do logic exercises to learn the natural deduction system from *"Logic: Techniques of Formal Reasoning" by Kalish, Montague, and Mar.[2] The program is officially only for MacOS and Windows, but with a little work it's possible to get it running on Linux, as it's just Java. The exercises are fun, and the program will not only check your work to make sure it's right, but also point out where and sometimes why it's wrong. [1] - https://logiclx.humnet.ucla.edu/Logic/Download https://logiclx.humnet.ucla.edu/Logic/Download [2] - https://www.amazon.com/Logic-Techniques-Reasoning-Donald-Kalish/dp/0195155041 https://www.amazon.com/Logic-Techniques-Reasoning-Donald-Kal...

cortesoft 8y ago
Oh man, brings back memories. I used an earlier version of this program as a philosophy undergrad at UCLA in the early 2000s. I LOVED doing the homework in my logic classes!
nixpulvis 8y ago
I'm assuming that program is more approachable than something like Coq or others? I used ACL2 a bit in college, and could imagine people being frustrated trying to learn it on their own.
- pvarangot 8y ago
  It's infinitely more approachable than Coq/PVS or whatever other theorem prover since it was designed for teaching and not a research tool or potential application to actually verifying properties of complex systems.

nixpulvis 8y ago

I've been working my way through Kleene's "Mathmatical Logic". It's a great read so far, touching on the details and proofs in some detail. I'm looking forward to the chapters on completeness and the like. I was mostly inspired to get his book because of the Kleene star, who knows why. Also, though very different, I just got GEB for Christmas, so I guess I'll be reading that finally now too.

dang 8y ago

2017: https://news.ycombinator.com/item?id=15114139 https://news.ycombinator.com/item?id=15114139 2015: https://news.ycombinator.com/item?id=10819702 https://news.ycombinator.com/item?id=10819702

nixpulvis 8y ago
Off topic: I'm honestly kinda surprised this kind of comment isn't built into HN by this point. There's often so many good comments from old articles we rely on adventurous users to dig up.
- barry-cotter 8y ago
  It is. Ctrl + F “past” and you’ll see it between hide and web up top.

BucketSort 8y ago

Fyi, there are many correspondences between logic and type theory / functional programming. I have found that as a programmer, many ideas are more accessible to me in type theory as opposed to logic. Languages like Haskell are great for exploring these relationships. This is also known as computational trinitarianism - https://ncatlab.org/nlab/show/computational+trinitarianism https://ncatlab.org/nlab/show/computational+trinitarianism Robert Harper, the computer scientist that coined "computational trinitarianism," has a series of lectures on the foundations of type theory including some commentary on these correspondences - https://youtu.be/9SnefrwBIDc https://youtu.be/9SnefrwBIDc.

_emacsomancer_ 8y ago
> many ideas are more accessible to me in type theory as opposed to logic But how do you understand type theory without some basic understanding of logic?
- BucketSort 8y ago
  It's possible, but I guess I should have specified "logic outside the standard curriculum of computer science studies." For example, I think understanding bits of modal logic through how monads behave is much more fruitful for a CS person. Also, I want to further add here that the correspondence between proofs and programs is known as the Curry–Howard correspondence. This is the more general term under which these relationships between type theory and logic are discussed. The term "computational trinitarianism" also adds a further correspondence to categories. ( As shown in my link above ).
  - BucketSort 8y ago
    Also, "Curry–Howard–Lambek correspondence" is the real name for "computational trinitarianism." I like the latter better because I don't like naming mathematical things after people, which have no bearing on the actual meaning.
  - _emacsomancer_ 8y ago
    Ok, but students need to understand at least ¬, ∧, ∨, →, and there are other useful equivalencies as between sets and (characteristic) functions etc.

olooney 8y ago

This guide covers many different topics and specialties related to logic so it may help to introduce a taxonomy so we don't get intimidated by the breadth of Dr. Smith's scholarship. Let's break it down into 5 topics: 1. Using a well-known and widely accepted system of logic to produce proofs and solve problems. A working man's logic is propositional logic (AND, OR, NOT, and the material conditional) plus first-order predicate logic (quantifiers "there exits" and "for all" over bound variables), natural deduction, and ZFC set theory. 2. "non-standard" logic systems which are somehow "better" or "more expressive:" 2nd order logics, modal logics, many-valued logics, etc. 3. Meta-mathematical investigations into the properties of different formal logic systems: model theory, proof theory, forcing, consistency, completeness, etc. 4. The philosophy of logic: Semantics, sense/reference, truth, nominalism/realism, theory of descriptions, etc. 5. Logic and computability: lambda calculus, recursive functions, turing machines, complexity classes, etc. This is somewhat tangential to logic proper but there are connections and Dr. Smith has a section on it so it's worth enumerating. While everyone will need to know (1) as a working man's logic, the other topics are more or less independent and can be approached independently. For people just starting out and finding this study guide pretty overwhelming, let me re-emphasize two of Dr. Smith's suggestions for starting points: Smullyan's First Order Logic and Halmos's Naive Set Theory. These two books will get you to the same depth of understanding that 95% of working mathematicians need or apply in their day-to-day work, and it's a fact that 95% of modern mathematical theories are built on (formalized within) ZFC set theory and first order logic. https://en.wikipedia.org/wiki/Naive_Set_Theory_(book) https://en.wikipedia.org/wiki/Naive_Set_Theory_(book) http://store.doverpublications.com/0486683702.html http://store.doverpublications.com/0486683702.html I also suggest the online game The Incredible Proof Machine. It's extremely helpful to have a computer formally check your proofs when you're just starting out in logic because it's incredibly easy to "cheat" and skip steps or use rules that "make sense" but aren't part of the formal system your using. TIPM lets you do that without learning any specialized syntax. http://incredible.pm/ http://incredible.pm/

topynate 8y ago

I've been following this guide for several months. It's made some excellent recommendations so far. Prospective type theorists, students of linear logic, etc. will have to venture beyond the reading list, but having a good grasp of the modern fundamentals of logic has made a big difference to me in how well I can follow texts like HoTT.

jesuslop 8y ago

And for leisure, www.logicomix.com (a surprising graphical novel bio-"pic" of Russell and some episodes of the foundations saga).

edoo 8y ago

Studying logic taught me one of the more important distinctions in life is identifying when things are always true vs sometimes true. We are taught to often group things that are mostly true into the always true category. This is effectively lossy compression that can introduce serious error into your line of reasoning.

nurettin 8y ago
That doesn't make sense to me as in real life most of our reasoning comes from syllogisms for practical reasons. And if something is consistently demonstrated to be true, chances are it will continue to be so, so we take our chances with that. It isn't lossy anything, it is life.
- claudiawerner 8y ago
  As a side note, it's always kind of funny to see hackers/computer types try and frame discussions in terms of things which are familiar to them, and these comments are often highly upvoted because of the explanation. In this instance, "lossy compression". But few people ever seem to question whether the domain of such categorisations is at all applicable to real human situations, and even if it's possible to make such categorisations. Is the method of the natural sciences or mathematics applicable identically to the social sciences? Often hackers assume this to be the case. I think there's also an element that hackers want to feel as though using the concepts they've developed which are very powerful in computer science should therefore be key to understanding the world as a whole. It's partially being eager to apply one's knowledge and partly hubris and unwillingness to defer to philosophy, sociology or critical theory which they view as less rigorous (and therefore bad).
  - hnuser1234 8y ago
    Why is it funny that people understand things in terms of their experience? The original comment about "lossy compression" essentially stated that humans don't have perfect thinking/memory/processing of probabilities. Do you disagree? Does it matter whether or not the wording of this idea uses computer science terms? Sure, technical people might try to apply methods from technical disciplines to social ones. Sometimes it works, sometimes it doesn't. As a rule, however, I don't think anyone assumes mathematics will completely replace social studies. We might use statistics to better understand social studies, but the social context is still distinctive from pure math, and always will be. Some of the best hackers are the ones who DO borrow ideas from other disciplines. And all other disciplines can often benefit from applying increasingly complex statistical methods, aided by computer and data scientists.

alphakilo 8y ago

On pages 43-44, the author mentions a member of my school's faculty G. Toualakis. The criticisms are valid and his textbook is convoluted. I appreciate the recognition on unnecessary formalism and complexity. For a 1000 level logic course that Software Engineers, Computer Engineers and Computer Science must take, it is extreme. Overall, interesting to see!

bsznjyewgd 8y ago
The author is refering to a different Tourlakis text than the one used in the 1000 level logic course for compsci students.

james_s_tayler 8y ago

This is a pretty epic map. Does anyone know of any others for other domains of knowledge??

khrm 8y ago

A much shorter guide by the same author in 2 pages instead of 90: https://www.logicmatters.net/tyl/shorter-tyl/ https://www.logicmatters.net/tyl/shorter-tyl/

bostonvaulter2 8y ago

Is there an ePub version of the guide available anywhere?