Natural Deduction for Intuitionistic Logic | Attic Philosophy

Поделиться
HTML-код
  • Опубликовано: 13 дек 2024

Комментарии • 26

  • @thimblequack
    @thimblequack Год назад

    Great videos. What books/articles would you recommend if I want to use intuitionistic logic in my essays?

  • @vitusschafftlein77
    @vitusschafftlein77 3 года назад +2

    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
      @AtticPhilosophy  3 года назад +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
      @biblebot3947 Год назад

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

    • @AtticPhilosophy
      @AtticPhilosophy  Год назад

      @@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
      @biblebot3947 Год назад

      @@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
      @AtticPhilosophy  Год назад

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

  • @alexandersanchez9138
    @alexandersanchez9138 2 года назад +1

    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
      @AtticPhilosophy  2 года назад

      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.

  • @EmC-p2y
    @EmC-p2y 10 месяцев назад

    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
      @AtticPhilosophy  9 месяцев назад +1

      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.

    • @EmC-p2y
      @EmC-p2y 9 месяцев назад

      @@AtticPhilosophy Thanks

  • @chiragsejpall
    @chiragsejpall Год назад

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

    • @AtticPhilosophy
      @AtticPhilosophy  Год назад

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

  • @desent493
    @desent493 2 года назад

    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
      @AtticPhilosophy  2 года назад +1

      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
      @desent493 2 года назад

      @@AtticPhilosophy thanks!

  • @danielconiff8178
    @danielconiff8178 3 года назад +1

    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
      @AtticPhilosophy  3 года назад +1

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

    • @nineironshore
      @nineironshore 8 месяцев назад

      @@AtticPhilosophy yeah but do modal metaphysics

  • @tomholroyd7519
    @tomholroyd7519 2 года назад

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

  • @ericericsson3592
    @ericericsson3592 2 года назад

    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
      @AtticPhilosophy  2 года назад

      I know! Nothing I can do about the old videos, it’s much lower in the newer ones.

  • @JokesandJesters
    @JokesandJesters 3 года назад

    can i get your socials i have a lot of questions for you

    • @AtticPhilosophy
      @AtticPhilosophy  3 года назад

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