Open Logic Project(builds.openlogicproject.org)
builds.openlogicproject.org
Open Logic Project
http://builds.openlogicproject.org/
19 comments
Has anyone here taught out of any of these, or tried working through any of them? I'd be very interested in comments, general or specific. (I am starting up a Logic class at my school.)
I read many sections of a few volumes when trying to pick a textbook to teach a seminar in Oxford. They are really nice, which is not surprising as they have e.g. Jeremy Avigad in the editorial board. Furthermore, they are beautifully typeset. I required a more computational approach, so my favorite texts remain:
* https://link.springer.com/book/10.1007/978-0-8176-4763-6
* https://www.cs.bham.ac.uk/research/projects/lics/
* https://link.springer.com/book/10.1007/978-1-4471-4129-7
* https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...
The last one is freely available, but also quite advanced as it develops all theory from the Curry-Howard isomorphism angle. I think it is ideal for advanced CS students though, and an amazing textbook due to the breadth of material it manages to cover.
* https://link.springer.com/book/10.1007/978-0-8176-4763-6
* https://www.cs.bham.ac.uk/research/projects/lics/
* https://link.springer.com/book/10.1007/978-1-4471-4129-7
* https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...
The last one is freely available, but also quite advanced as it develops all theory from the Curry-Howard isomorphism angle. I think it is ideal for advanced CS students though, and an amazing textbook due to the breadth of material it manages to cover.
I took a class under one of the authors with "sets, logic, computation". I found this textbook to be incredibly good for both reading and as a reference. It presents things very straightforwardly (the language is simple) and clearly (makes good use of tables and diagrams to give the full info needed to understand something). The chapters are short and digestible. I forget if the text includes exercises, but I found the exercises in that class very good as well. I was actually looking for this text again, so that I could use it as a reference while learning Homotopy Type Theory, and here it is!
correction: I actually used the text "What If?" NOT "sets, logic, computation"! My mistake.
I would be very interested to understand how people use logic theories in day to day life or work?
Is this something which one can learn and use in other walks of life, for example programming or ML?
Edit:
What I often find is that reading this type of material seems very mentally stimulating, but these texts do not seem to offer any introduction or intuition as to why someone should learn this material or how to use it outside of the logic domain.
Is this something which one can learn and use in other walks of life, for example programming or ML?
Edit:
What I often find is that reading this type of material seems very mentally stimulating, but these texts do not seem to offer any introduction or intuition as to why someone should learn this material or how to use it outside of the logic domain.
> how to use it outside of the logic domain
You've got it backwards. Logic isn't a domain, just like algebra isn't a domain. Logic is what lets us work within a given domain. It isn't like geometry, which won't be useful unless you're working with shapes and angles; logics (and, more generally, algebras) are the syntax of entity relations.
In particular, logic is about "preserving truth between statements". That is, if we have a set of true statements, and we want to generate new true statements, logic is the way to do that, and it's always done in the same way, using arguments.
That word has two common meanings, but the arguments of logic are: premises, linked by deductive rules to conclusions. If the deductive rules are valid, and the premises are true, then the conclusions will deductively also be true. "Premises" can be any type of statement that has a truth-value (i.e. makes a claim about a fact).
So, obviously, this is the basis of all proofs, in any discipline. But it's also the foundation of rational persuasion, as in a court room. Which is to say that you're already using informal logic, every day. The question is "would it be useful in your life to learn these things formally?"
What's the difference between someone with the intuition "the opposite side of the 90° angle in a triangle is always the largest", versus someone who understands the Pythagorean theorem?
You've got it backwards. Logic isn't a domain, just like algebra isn't a domain. Logic is what lets us work within a given domain. It isn't like geometry, which won't be useful unless you're working with shapes and angles; logics (and, more generally, algebras) are the syntax of entity relations.
In particular, logic is about "preserving truth between statements". That is, if we have a set of true statements, and we want to generate new true statements, logic is the way to do that, and it's always done in the same way, using arguments.
That word has two common meanings, but the arguments of logic are: premises, linked by deductive rules to conclusions. If the deductive rules are valid, and the premises are true, then the conclusions will deductively also be true. "Premises" can be any type of statement that has a truth-value (i.e. makes a claim about a fact).
So, obviously, this is the basis of all proofs, in any discipline. But it's also the foundation of rational persuasion, as in a court room. Which is to say that you're already using informal logic, every day. The question is "would it be useful in your life to learn these things formally?"
What's the difference between someone with the intuition "the opposite side of the 90° angle in a triangle is always the largest", versus someone who understands the Pythagorean theorem?
But how do you know that "informal logic" has anything to do with formal logic? Outside of math, formal logic seems actively misleading. For example, the "principle of explosion" (from a contradiction follows anything) is definitely not how people think.
Philosophically, I prefer the reasonable / rational / meta-rational framework explained by David Chapman. [1] But if you want to know how people ordinarily think, better to study how they think.
(And in practical everyday use on the Internet, I find logic mostly useful for for shooting down attempts at inappropriately applying logic to conclude things that you can't safely conclude.)
[1] https://metarationality.com/reasonableness-aspects
Philosophically, I prefer the reasonable / rational / meta-rational framework explained by David Chapman. [1] But if you want to know how people ordinarily think, better to study how they think.
(And in practical everyday use on the Internet, I find logic mostly useful for for shooting down attempts at inappropriately applying logic to conclude things that you can't safely conclude.)
[1] https://metarationality.com/reasonableness-aspects
>the "principle of explosion" (from a contradiction follows anything) is definitely not how people think.
"Well then, if you believe that then you'll believe anything."
Sounds pretty folksy to me.
"Well then, if you believe that then you'll believe anything."
Sounds pretty folksy to me.
> Outside of math, formal logic seems actively misleading. For example, the "principle of explosion" (from a contradiction follows anything) is definitely not how people think.
It's generally very easy to find natural language constructs that rely on any given principle of formal logic. For the principle of explosion, an example would be "if you're thirsty, there's tea in the kitchen".
It's generally very easy to find natural language constructs that rely on any given principle of formal logic. For the principle of explosion, an example would be "if you're thirsty, there's tea in the kitchen".
I've used TLA+ extensively when designing distributed systems. It's a mathematical logic language for describing systems and verifying their properties.
It's more like a foundation for other types of material such as the theory of programming languages (which helps in understanding things like ML). Just about every paper or textbook in PLT relies on logic-based notation and concepts.
Having a more grounded understanding of logic, even a 101-level course understanding, can be really helpful in a technical job. I think reviewing materials like these, in combination with a basic understanding of Bayesian probability, has been very helpful when acting as a team lead or cross-team architect with my team of programmers.
It's ultimately stuff that feels obvious-in-hindsight and thus easy to undervalue, but for me it encompasses matters such as:
1) Making sure that a desired solution actually addresses an explicitly understood problem (other than "the problem is that the desired solution isn't in place!") This means being able to explicitly state the problem and symptoms as a state of current reality, separate from discussion of what the solution should be.
2) Resisting the urge to seize on the easiest-to-grasp potential cause of an effect (this is a big one with many programmers, I am constantly asking things like, "are you sure that's the only possible cause?" and "but if that were the cause, wouldn't this other effect, which is not happening, also be happening?") People can waste a lot of time chasing theories that don't fully explain the symptoms.
3) Constantly testing and updating mental models. For instance, I am frequently urging team members to state their expectations before running an experiment, rather than just "seeing what happens". For example, "now that I have set this configuration value, I expect to see this effect". This is to guard against the "let's just hack until it seems to work" phenomenon, which is a recipe for introducing latent bugs from not understanding the whole system/model.
4) Better communication! Engineers have a habit of speaking in shorthand, causing other people to say, "Wait, can we back up a bit?" (Or worse, not doing so when they should.) Explicitly setting context up front, including explicitly stating assumptions up front, better sets the table for group discussions where everyone is on the same page. Under-communicating is more frustrating than over-communicating.
5) The final benefit of #4 is that if you are responsible about stating the premises/assumptions that lead to your conclusion, then you have effectively depersonalized the discussion. Such that, if through discussion you discover that a premise/assumption underlying a conclusion is incorrect, then you can easily switch gears. Since the conclusion flowed from that set of stated premises, rather than "Person X being adamant", then it is easier that Premise #3 is wrong than "Person X being wrong".
Anyway, all of these practices are easier to implement and follow if you have an appreciation for the kinds of logical concepts taught in basic logic courses.
It's ultimately stuff that feels obvious-in-hindsight and thus easy to undervalue, but for me it encompasses matters such as:
1) Making sure that a desired solution actually addresses an explicitly understood problem (other than "the problem is that the desired solution isn't in place!") This means being able to explicitly state the problem and symptoms as a state of current reality, separate from discussion of what the solution should be.
2) Resisting the urge to seize on the easiest-to-grasp potential cause of an effect (this is a big one with many programmers, I am constantly asking things like, "are you sure that's the only possible cause?" and "but if that were the cause, wouldn't this other effect, which is not happening, also be happening?") People can waste a lot of time chasing theories that don't fully explain the symptoms.
3) Constantly testing and updating mental models. For instance, I am frequently urging team members to state their expectations before running an experiment, rather than just "seeing what happens". For example, "now that I have set this configuration value, I expect to see this effect". This is to guard against the "let's just hack until it seems to work" phenomenon, which is a recipe for introducing latent bugs from not understanding the whole system/model.
4) Better communication! Engineers have a habit of speaking in shorthand, causing other people to say, "Wait, can we back up a bit?" (Or worse, not doing so when they should.) Explicitly setting context up front, including explicitly stating assumptions up front, better sets the table for group discussions where everyone is on the same page. Under-communicating is more frustrating than over-communicating.
5) The final benefit of #4 is that if you are responsible about stating the premises/assumptions that lead to your conclusion, then you have effectively depersonalized the discussion. Such that, if through discussion you discover that a premise/assumption underlying a conclusion is incorrect, then you can easily switch gears. Since the conclusion flowed from that set of stated premises, rather than "Person X being adamant", then it is easier that Premise #3 is wrong than "Person X being wrong".
Anyway, all of these practices are easier to implement and follow if you have an appreciation for the kinds of logical concepts taught in basic logic courses.
I definitely agree, but for your use cases wouldn't there be more appropriate texts like for example Meaning and Argument:
https://www.amazon.com/Meaning-Argument-Introduction-Through...
https://www.amazon.com/Meaning-Argument-Introduction-Through...
Thank you! That is extremely helpful.
[deleted]
This stuff is foundational to things that check for program correctness. For examples type checkers check if the program is type correct. The foundations of these checkers rest on the content of these pages.
It goes even further then this in the sense that with logic you can design a language with correctness checking where even the logic of your entire program can be verified via something similar to a type check. So for example, Agda or Idris are examples of languages with this capability.
So basically most of this stuff isn't relative to most job. It's a higher level thing. It's more advanced theory for the people who create the tools SO you can do your job. A step above Dev Ops... it's the people who create the languages you use.
It goes even further then this in the sense that with logic you can design a language with correctness checking where even the logic of your entire program can be verified via something similar to a type check. So for example, Agda or Idris are examples of languages with this capability.
So basically most of this stuff isn't relative to most job. It's a higher level thing. It's more advanced theory for the people who create the tools SO you can do your job. A step above Dev Ops... it's the people who create the languages you use.
Do these books also have an accompanying solution manual?
I couldn't find them on the website. I'd love to work my way through these books. However, I'm afraid the reality will be that I'll get stuck on solution, can't figure it out within an hour, and lose motivation.
I couldn't find them on the website. I'd love to work my way through these books. However, I'm afraid the reality will be that I'll get stuck on solution, can't figure it out within an hour, and lose motivation.
Related:
Open Logic Project: An Open-Source, Collaborative Logic Text - https://news.ycombinator.com/item?id=17739248 - Aug 2018 (8 comments)
The Open Logic Project - https://news.ycombinator.com/item?id=9961863 - July 2015 (12 comments)
Open Logic Project: An Open-Source, Collaborative Logic Text - https://news.ycombinator.com/item?id=17739248 - Aug 2018 (8 comments)
The Open Logic Project - https://news.ycombinator.com/item?id=9961863 - July 2015 (12 comments)
This link goes to http://builds.openlogicproject.org/ which explains nothing.
Why not link to http://openlogicproject.org/