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!

@AtticPhilosophy

3 жыл бұрын

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

8 ай бұрын

@@AtticPhilosophyit is truth functional, but no finite Heyting Algebra can capture all intuitionist validities

@AtticPhilosophy

8 ай бұрын

@@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).

@biblebot3947

8 ай бұрын

@@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.

@AtticPhilosophy

8 ай бұрын

@@biblebot3947 It means there's a *finitely specifiable* function on truth-values. So equivalently: there's a (finite valued) truth-matrix.

Hey, I looked at your academic philosophy page and saw that you are interested in metaphysics. Could you make a video on it sometime?

@AtticPhilosophy

3 жыл бұрын

Sure, I haven't done much metaphysics on this channel yet, but definitely will do in the future.

@nineironshore

3 ай бұрын

@@AtticPhilosophy yeah but do modal metaphysics

Great video! Is removing the indirect proof rule from first order logic enough to give a sound proof system for first order intuitionistic logic?

@AtticPhilosophy

2 жыл бұрын

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)

@desent493

2 жыл бұрын

@@AtticPhilosophy thanks!

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

@AtticPhilosophy

5 ай бұрын

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.

@user-wt7vb4yv1s

4 ай бұрын

@@AtticPhilosophy Thanks

how would you do constructive natural deduction for (Av not B) -> B -> A ?

@AtticPhilosophy

11 ай бұрын

Assume Av~B, assume B, then use v-elim to infer A.

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)

@AtticPhilosophy

2 жыл бұрын

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

@AtticPhilosophy

2 жыл бұрын

Have a look in the description - or leave questions here in the comments. (New comments are easiest to see!)

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.

@AtticPhilosophy

Жыл бұрын

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.

Logic is a closed symmetric monoidal category. Implication is right adjoint to conjunction (called fusion). Negation is an involution, Possibly is a monad.

@AtticPhilosophy

Жыл бұрын

Maybe, it Depends on the logic.