I think this article has a lot of potential to be helpful. I would love to see (hear) a version of the video where the speech was not auto-generated but delivered by a human narrator. The auto-speech is done well as such things go, and it's fine for motivated viewers. But if I show this video to my kids, or to a class of students, they will be more engaged if they hear a real person speaking with understanding and intentionality.
I mean sure, but that's only if you define phi to be the condition and psi to be the statement of the code in the if-clause. But you could have psi be the statement "the lines in the then-branch will be executed" and that way the else-clause corresponds to "the lines in the else-branch will be executed", which corresponds to "not phi". Edit: switched "condition" to "branch"
Sure, you could define such a predicate (which would likely have additional arguments, such as program state and more). But then you would have an iff, not an implication.
@@TrulyUnderstandingAlgorithms Oh yeah, you're 100% right. There's never a case in which the then-branch is executed while the condition is false. My bad 😅
I would love SO MUCH if someone would teach in the style of 3blue1brown comprehensively type theory and the proof theory used in type theory papers. This field is so inaccessible especially if you have a lack of prerequisite math knowledge and logic knowledge and don't know what you don't know. Most teaching materials is full of assumed knowledge and unless studying with someone who actually does it you will have such a hard time just by reading some of the few books that exist on it.
@@TrulyUnderstandingAlgorithms Can you recommend please in that case books that properly fill the gaps for all prerequisites that are needed for learning type theory and the form of proof theory used in type theory? Either as a response to my comment or a blog post. I have not found any study guide outlines for these areas I'm interested in.
That is actually a good question. I'm not sure what the best start guide to type theory would be. Most material seems to be rather advanced. Perhaps some reader could step in and make some recommendation?
Implies tends to show up quite a bit in propositional logic, but doesn't seem to be as common in boolean algebra, or at least not in programming. Aside from if-then operations, what _is_ seen more often in programming is and-not, which in boolean algebra is written as a ∧ ¬b, or in many programming languages as either a & !b or a && !b. This can actually be written in terms of implication as ¬(a → b), and is also closely related to the set difference A ∖ B. Really, the problem with logical implication is just that it's worded as "if a then b." This kind of phrasing is very common in natural, causal, non-logical language, that in a way it's more _mathematicians'_ fault that the confusion exists by overloading this phrase and insisting it means something that it wouldn't in natural language. Yes, the two meanings have overlap, but they're clearly not the same and probably should never have been said the same. If-then operations in programming correspond much more closely to the natural meaning of the phrase. (And-not does not have this issue since it's much less common in natural usage and might even sound strange outside of formal contexts.)
Implication x→y is simply (!x || (x && y)) Either x is false, so y can be anything. Or x is true, and y is true. Otherwise if y is false when x is true, the proposition would be false. I think there's no programming equivalent to this boolean logic. However there is iff behavior (equivalence) x ←→ y. Simply x == y. (Where x and y are boolean obviously) And the inverse x != y where they must differ. Or simply using a XOR. There's many x and y binary operators resulting in boolean result truth tables, but implication, being one of them is somewhat more interesting than no matter what x and y are it's either true, false, x, or y as output. Implication, and, or, xor, xnor, nor, nand, those actually care about both inputs are interesting.
This video takes me back to my 6th grade math class, when we spend the entire second half of the year on propositional logic.
Hopefully in a good way :)
I think this article has a lot of potential to be helpful. I would love to see (hear) a version of the video where the speech was not auto-generated but delivered by a human narrator. The auto-speech is done well as such things go, and it's fine for motivated viewers. But if I show this video to my kids, or to a class of students, they will be more engaged if they hear a real person speaking with understanding and intentionality.
Love the video!
Glad you enjoyed it!
I mean sure, but that's only if you define phi to be the condition and psi to be the statement of the code in the if-clause.
But you could have psi be the statement "the lines in the then-branch will be executed" and that way the else-clause corresponds to "the lines in the else-branch will be executed", which corresponds to "not phi".
Edit: switched "condition" to "branch"
Sure, you could define such a predicate (which would likely have additional arguments, such as program state and more). But then you would have an iff, not an implication.
@@TrulyUnderstandingAlgorithms Oh yeah, you're 100% right. There's never a case in which the then-branch is executed while the condition is false. My bad 😅
I would love SO MUCH if someone would teach in the style of 3blue1brown comprehensively type theory and the proof theory used in type theory papers.
This field is so inaccessible especially if you have a lack of prerequisite math knowledge and logic knowledge and don't know what you don't know. Most teaching materials is full of assumed knowledge and unless studying with someone who actually does it you will have such a hard time just by reading some of the few books that exist on it.
That would be a niche, but very nice project!
@@TrulyUnderstandingAlgorithms Can you recommend please in that case books that properly fill the gaps for all prerequisites that are needed for learning type theory and the form of proof theory used in type theory? Either as a response to my comment or a blog post. I have not found any study guide outlines for these areas I'm interested in.
That is actually a good question. I'm not sure what the best start guide to type theory would be. Most material seems to be rather advanced. Perhaps some reader could step in and make some recommendation?
Implies tends to show up quite a bit in propositional logic, but doesn't seem to be as common in boolean algebra, or at least not in programming. Aside from if-then operations, what _is_ seen more often in programming is and-not, which in boolean algebra is written as a ∧ ¬b, or in many programming languages as either a & !b or a && !b. This can actually be written in terms of implication as ¬(a → b), and is also closely related to the set difference A ∖ B.
Really, the problem with logical implication is just that it's worded as "if a then b." This kind of phrasing is very common in natural, causal, non-logical language, that in a way it's more _mathematicians'_ fault that the confusion exists by overloading this phrase and insisting it means something that it wouldn't in natural language. Yes, the two meanings have overlap, but they're clearly not the same and probably should never have been said the same. If-then operations in programming correspond much more closely to the natural meaning of the phrase. (And-not does not have this issue since it's much less common in natural usage and might even sound strange outside of formal contexts.)
Thanks for this insightful comment! Interestingly, the and-not connective is equivalent to the negation of implication.
Implication x→y is simply (!x || (x && y))
Either x is false, so y can be anything.
Or x is true, and y is true.
Otherwise if y is false when x is true, the proposition would be false.
I think there's no programming equivalent to this boolean logic. However there is iff behavior (equivalence) x ←→ y. Simply x == y. (Where x and y are boolean obviously)
And the inverse x != y where they must differ. Or simply using a XOR.
There's many x and y binary operators resulting in boolean result truth tables, but implication, being one of them is somewhat more interesting than no matter what x and y are it's either true, false, x, or y as output. Implication, and, or, xor, xnor, nor, nand, those actually care about both inputs are interesting.
Good summary!