Logic 4: Natural Deduction with Logical Axioms - Tutorial 4/4

[@Bisqwit]

*The complete list of introduction & elimination rules can be found in the video description.* This video was originally supposed to end at about 20:10. But then I decided that adding more examples would be probably quite helpful on this difficult topic, so I extended the video. Unfortunately, a burnt PSU (which warranty covered) also took out the harddrive on which all the video originals were (and the warranty didn’t cover this), so I could not use the same graphics template anymore. This is why the second part of the video, after 20:10, is so different to the previous one. The subtitles differ sometimes from the spoken text. In those cases, the subtitles are usually correct; they indicate what I _intended_ to say, correct spoken mistakes.

[@AT-zr9tv]

There is something oddly satisfying in proving these somewhat obvious claims with such extreme rigor. Very fun and nerdy. Your videos are great!

[@Bisqwit]

Yeah, mathematical proofs are like that. Sometimes the claim seems obvious and the proof is complicated; sometimes the claim is not very obvious at all, and the proof is equally satisfying. The proof that √2 is irrational (not a ratio of two integers, however large) falls into the latter category in my opinion. Thank you!

[@AT-zr9tv]

@@Bisqwit One fun way of highlighting that all these logical proofs aren't so "obvious", is to change an axiom, and see all the logical ramifications that follow. You end up with a very, very different set of rules, like a parallel world of logic that isn't ours! Perhaps you could do this as a fun bonus video?

[@Bisqwit]

Thanks. Do you have an example in mind?

[@Elias07070]

Even though I probably can follow 1% of what is said here, I can watch it again and again and learn a little bit more than the last time, a gold mine of knowledge that keeps on giving

[@TheMimoJimi]

Wow, love you new logo! God bless!

[@pointerish]

Thank you for creating this series. It's been awesome.

[@nathanielbarragan882]

I find it interesting that when doing normal mathematical proofs, it grows downward (and usually right) as you do your work, logic grows upward (and usually right) as you do your work.

[@Bisqwit]

It is just easiest in my opinion to work from bottom up, but the deductions can be performed in either order if you know what you are working towards.

[@wonggran9983]

Even if can deduce a lot of logical truths from basic axioms, I've seen in my natural deduction class deducted sentences that are translated in English from the basic English sentence axioms for the class lecture being questioned, even when the rules of deduction are shown to be correct using symbols A, B. Other students QUESTION the logically deduced sentences from basic axioms/assumptions EVEN when the rules that were used to deduce the sentences from the basic axioms are SHOWN MECHANICALLY to be correct.

[@wonggran9983]

6:39 A -> B A implies B. A is true then if the sentence is correct which it is because it's there, then B is true. If A is false then B cannot be concluded which can be said as false because implication is not dependency assuming B is an event.

[@emmettdja]

every time he says exestential quantifier it reminds me that I have no idea what is happening.

[@codework-vb6er]

@Bisqwit May I ask what textbook or references explain this. I would like to do more examples.

[@Bisqwit]

Here are some references that I used in my bachelor’s thesis about natural deduction. @book{lemmon, place={London u.a.}, title={Beginning logic}, publisher={Chapman \& Hall}, author={Lemmon, Edward J.}, year={1992}} @book{salminen, place={Helsinki}, title={Johdatus Logiikkaan}, publisher={Gaudeamus}, author={Salminen, Hannele and Väänänen, Jouko}, year={1992}} @book{prawitz, place={Stockholm u.a.}, title={Natural deduction}, publisher={Almqvist & Wiksell}, author={Prawitz, Dag}, year={1965}} @book{elements, title={The elements of mathematical logic}, publisher={Dover}, author={Rosenbloom, Paul C.}, year={1950}}

[@codework-vb6er]

@@Bisqwit Thank you ♥

[@spudwish]

I've seen similar notation when trying to study operational semantics (I gave up very quickly), is it the same notation?

[@Bisqwit]

I have never heard of structural operational semantics. Perusing Wikipedia and image search quickly, it seems that the only similarity is the use of horizontal lines. In natural deduction, you put above the line the facts, below the line the conclusion and after the line a brief explanation of which operation you introduced or eliminated. You stack these operations as needed, in order to construct a deduction from axioms. In doing so, you form a tree of conclusions. In operational semantics, you put above the line a description of a program state and a condition, and below the line an indication how the program state is changed when that condition is met. I could not find evidence that these lines are ever stacked. They are always isolated.

[@Veso266]

I have a question (its not about logic, so I hope its fine) I was wondering if you maybe still have your std:vector implementation for Bordland C++ somewhere In the terminal series, you showed a part of your dos terminal and in there was a (it seams) nice std:vector implementation for Bordland, cuz bordland doesn't have that and I would sure like to use it for something) BTW: how are your studies going? I being a practical person find it very hard to learn theoretical subjects if they are not connected with practise and sadly some subject just aren't, (and I don't mean solving example problems that make no sense in real word practise, I mean real practise :) ) you have to first learn theory to be able to do pratcties (to be able to assume properly and to be able to do practise right), so how do you keep your attention when learning this theoretical subjects?

[@WilliamDye-willdye]

Before going into a long math proof, it might help to give an example of why we bother to be so rigorous. The example I use on myself is parallel lines. Even mathematicians mostly gave up and shrugged "well, it's just obvious". Then it turns out the universe is non-Euclidian.

[@Bisqwit]

In a previous episode, I showed that a truth table can be used to prove that a proposition is identical with another proposition. That does not work with predicate logic though. It needs another method, and I introduced that in this episode. Although, to be honest, this method does not prove that a predicate sentence is identical with another one. Rather, this method proves _if_ we know some predicate sentences, _then_ another predicate sentence is valid. In other words, while a truth table proves that sentences A and B are equivalent, the natural deduction only proves that A implies B. (A might also be absent, in which case the natural deduction just proves that B is self-coherent.)

[@a544jh]

I would have needed this video five years ago lol

[@mikefulli]

Maybe I'll try get into Prolog again after these. Have bounced off from it 5-6 times I have tried learning it previously. :D

[@ashwinalagiri-rajan1180]

Hey bisqwit, unrelated request: I saw your video on the typing game game that you made. I really liked it. Would you mind if I tried making that in HTML/Javascript with attribution of course.

[@Bisqwit]

You are free to make a clone of it, if you wish. After all, WSpeed is likewise a clone of ZTSpeed. Go ahead!

[@ashwinalagiri-rajan1180]

@@Bisqwit Thanks!

[@Bisqwit]

Have you made progress?

[@huistelefoon5375]

Hello, apologies, this question is not entirely related to this video. I am a young programmer with interest in low level systems, and also somewhat of a retro enthusiast. With my studies starting to pick up some pace, and I am no longer sure how to dedicate my time. I am afraid that if I dedicate my time purely as a hobbyist, that I might not pick up any useful skills to make a living. I am also somewhat afraid that programming as a job could take away the fun of my hobby, and leave me with no time to make fun projects, or perhaps even make videos. Do you think it is wise for me to find work in IT?

[@Bisqwit]

Both of your situations are probably true to some extent. There are no right or wrong choices in that aspect.

[@roberttalada5196]

Oh wow, thank you for these.

[@AtomSymbol]

Assuming FOO, whatever FOO is, and then pseudo-magically omitting any equivalent of FOO as an assumption in the final result is an _invalid_ mathematical step. It is thus logical/fitting that the procedure of Natural Deduction presented in the video _cannot_ be used to program computers.

[@Bisqwit]

I don’t quite understand what you are trying to say. But there was an annotation that explains what the purpose of assumptions is. Assumptions are a rhetoric device to justify things. If you know that A or B is true, but you don’t know which; then, if assuming that A is true leads into C being true as well, and by assuming that B is true also leads into C being true as well, then you know that no matter what, C must be true.

[@vasyanchichek]

Hi, friend! I'm sorry to write here, I need help to build Castlevania 2 ROM on UOROM mapper

[@Bisqwit]

ok

[@vasyanchichek]

@@Bisqwit Wrote you on Twitter

[@yasurikressh8325]

It was all smooth sailing until one could deduce that somehow {A->B, A} was followed by some random C implying B in short; {A->B, A} |- {C->B} but whyyyy?

[@Bisqwit]

Remember the example from episode 1: _"If there is a thief (C), the dog will bark (B)"._ If the dog barks (B), the implication is valid, regardless of whether there is a thief or not (C). From the premises, we can see that B must be true. So, the dog barks, and the existence of a thief is irrelevant; the implication is proven valid. It might be easier to understand if there was C∨B instead of C→B. If B is true, C∨B is also true regardless of value of C. However, C∧B would be true only if _both_ B and C are true. An implication C→B is true if B is true or if neither is true.

[@metaorior]

Please do c++ for beginners

[@emmettdja]

This is like regex, but for english...

[@wonggran9983]

There are no semantics in logic or natural deduction courses.

[@wonggran9983]

But if there are semantics from a deduction hoorae

[@ooze9808]

Why does your "how fast does bisqwit type" video have so many views?

[@Bisqwit]

Beats me.

[@maciej12345678]

did you fear of war with Russia?

[@Bisqwit]

I am not fearful, but I think that 1. Russia cannot be trusted; their declarations of intentions are absolutely worthless. 2. Russia has an expansionist imperial tendency, and they have attacked Finland before. In my opinion, there is a high probability that Russia will attack Finland some day. When that happens, I have no idea. Could be this year, could be two years from now, could be within 20 years. And seeing that Russia‘s war-conducting style nowadays seems to involve the principle “destroy everything, don’t care what it is, just destroy it”, it would be devastating to Finland.

[@maciej12345678]

@@Bisqwit you are close to Petersburg and estonia. Yep that same technic like in Syria.

[@ooze9808]

Boring, back to cpp please

[@Bisqwit]

Thank you for your rude input. Will do, but as my available free time has been pretty close to zero throughout this year, and I was quite fascinated with the logic courses, I decided to create this logic series in the break during new year, so I can publish these four episodes during the spring, so that my channel would not be totally devoid of content while I cannot make new videos due to lack of time. Better to have something than nothing.

[@ooze9808]

@@Bisqwit I apologize

[@FromFallToFlight]

loving your content