Great video! One question: At 12:15 you say that it doesn't make sense to use truth-tables in intuitionistic logic. Can you explain or will you talk about this in an upcoming video? Keep up the good work!
Thanks! Intuitionistic logic isn't truth-functional: we can't work out the value of ~A, or A->B, just by knowing the values of A and B. For example, the only sensible truth-function for negation in logics with 2 truth-values takes T to F and F to T. But then either A or ~A would always be T, and so Excluded Middle, Av~A, would be valid (always T). That's exactly what Intuitionistic logic wants to avoid. It's a bit like the situation with modal logic: the truth-value of A doesn't help with the truth-value of []A. In fact, you can think of Intuitionistic Logic as a kind of modal logic (S4 with some special principles added).
@@biblebot3947 Did you mean no *finite truth matrix* can capture intuitionistic validity? That's true - but that's what it means to say intuitionistic logic isn't truth-functional! For propositional intuitionistic logic, finite Heyting algebras are fine for evaluating validity (since the logic is decidable).
@@AtticPhilosophy I thought truth functional meant that connectives’ truth values are only a function of their inputs’ truth values instead of a syntactic property of them.
Here’s a fun fact: you can still derive “(not not not A) arrow (not A)” in intuitionistic logic. Here’s the proof: Suppose not not not A. Suppose A. Suppose not A; contradiction, so conclude not not A (in the scope of A). However, that’s a contradiction (in the scope of A); conclude, in the scope of not not not A, that not A holds, as desired.
Yes absolutely, and more generally, you can eliminate pairs of negations as long as you have some left. Figuratively, ~~~p to ~p is ok, by constructive lights, as you’re not getting something positive from something negative.
The X rule is needed. For ~I, it depends how negation is treated. If it’s a primitive symbol, you need ~I as a rule. But sometimes ~A is defined as A->F (F the falsom constant), in which case, the ->I rule will do for introducing negations.
That’s right, so long as you’re got in & out rules for all of the connectives & quantifiers (so you don’t introduce any of them by their classical equivalences)
Logic is a closed symmetric monoidal category. Implication is right adjoint to conjunction (called fusion). Negation is an involution, Possibly is a monad.
Great videos in general, really appreciate them; but omg the music, turn down the volume please, I totally jump scare every time at the beginning and end (don’t mind the music as such though, just the volume)
Great videos. What books/articles would you recommend if I want to use intuitionistic logic in my essays?
Great video! One question: At 12:15 you say that it doesn't make sense to use truth-tables in intuitionistic logic. Can you explain or will you talk about this in an upcoming video? Keep up the good work!
Thanks! Intuitionistic logic isn't truth-functional: we can't work out the value of ~A, or A->B, just by knowing the values of A and B. For example, the only sensible truth-function for negation in logics with 2 truth-values takes T to F and F to T. But then either A or ~A would always be T, and so Excluded Middle, Av~A, would be valid (always T). That's exactly what Intuitionistic logic wants to avoid.
It's a bit like the situation with modal logic: the truth-value of A doesn't help with the truth-value of []A. In fact, you can think of Intuitionistic Logic as a kind of modal logic (S4 with some special principles added).
@@AtticPhilosophyit is truth functional, but no finite Heyting Algebra can capture all intuitionist validities
@@biblebot3947 Did you mean no *finite truth matrix* can capture intuitionistic validity? That's true - but that's what it means to say intuitionistic logic isn't truth-functional! For propositional intuitionistic logic, finite Heyting algebras are fine for evaluating validity (since the logic is decidable).
@@AtticPhilosophy I thought truth functional meant that connectives’ truth values are only a function of their inputs’ truth values instead of a syntactic property of them.
@@biblebot3947 It means there's a *finitely specifiable* function on truth-values. So equivalently: there's a (finite valued) truth-matrix.
Here’s a fun fact: you can still derive “(not not not A) arrow (not A)” in intuitionistic logic.
Here’s the proof:
Suppose not not not A. Suppose A. Suppose not A; contradiction, so conclude not not A (in the scope of A). However, that’s a contradiction (in the scope of A); conclude, in the scope of not not not A, that not A holds, as desired.
Yes absolutely, and more generally, you can eliminate pairs of negations as long as you have some left. Figuratively, ~~~p to ~p is ok, by constructive lights, as you’re not getting something positive from something negative.
Are the ~I and X rules needed as well (in the classical logic video, they were redundant)? I would truly appreciate an answer for this
The X rule is needed. For ~I, it depends how negation is treated. If it’s a primitive symbol, you need ~I as a rule. But sometimes ~A is defined as A->F (F the falsom constant), in which case, the ->I rule will do for introducing negations.
@@AtticPhilosophy Thanks
how would you do constructive natural deduction for (Av not B) -> B -> A ?
Assume Av~B, assume B, then use v-elim to infer A.
Great video! Is removing the indirect proof rule from first order logic enough to give a sound proof system for first order intuitionistic logic?
That’s right, so long as you’re got in & out rules for all of the connectives & quantifiers (so you don’t introduce any of them by their classical equivalences)
@@AtticPhilosophy thanks!
Hey, I looked at your academic philosophy page and saw that you are interested in metaphysics. Could you make a video on it sometime?
Sure, I haven't done much metaphysics on this channel yet, but definitely will do in the future.
@@AtticPhilosophy yeah but do modal metaphysics
Logic is a closed symmetric monoidal category. Implication is right adjoint to conjunction (called fusion). Negation is an involution, Possibly is a monad.
Maybe, it Depends on the logic.
Great videos in general, really appreciate them; but omg the music, turn down the volume please, I totally jump scare every time at the beginning and end (don’t mind the music as such though, just the volume)
I know! Nothing I can do about the old videos, it’s much lower in the newer ones.
can i get your socials i have a lot of questions for you
Have a look in the description - or leave questions here in the comments. (New comments are easiest to see!)