Whenever I get confused in my uni logic studies, I can get clear explanations from your videos, in almost every topic. I love the clear way you explain things, you are my hero.
Amazing, I've been self-teaching myself formal logic for a little under a year and so far this has been more clear and informative an explanation of metalogic, soundness and completeness than what I've attempted to read in 6 intro textbooks and multiple youtube videos. Thank you.
Great to hear! I hear that a lot - often textbooks explain some topics (trees, or whatever) in lots of detail, then go on to prove something about those trees (or whatever) without explaining how those metalogic proofs work.
Most logic textbooks have some basic metalogic. Richard Jeffrey’s Formal Logic: Scope & Limits is old but excellent, it really simplifies completeness with tree proofs. The standard handbook of advanced results is Boolos & Jeffrey, Computability & Logic.
That particular proof seems very particular to binary systems. Supposes we draw from a sack of random sentences. We know what to do with truths, we keep 2 of them, and with any that evaluate as false we simply discard, but those in a 3rd state, we have no way to decide to keep or discard, so if we draw one from the sack, the procedure is stuck.
Great (and really helpful) explanation as usual. When I first got into contact with metalogic, we just went through the proofs without any backround information and I was really confused about what I was doing. The question I have is can you reason about all different logics the same way ? For example if I have a logic, where proof of contradiction doesn‘t work, can I use an informal version of that proof, when doing metalogic about that logic?
Great question! It really depends. We often reason classically about (e.g.) intuitionism or paraconsistent logic. That's fine if you're just trying to see how they work. It's also by far the easiest way to reason about a logic. But it's obviously not acceptable to committed (e.g.) intuitionists or dialethists. Giving an intuitionistic proof of intuitionistic completeness is much harder, since you have fewer rules to work with & it needs to be constructive. Reasoning about LP using just (extensional) LP would probably be impossible, since then you don't even have modus ponens! (You'd need at least to add a detachable conditional.)
Thanks! There’s some videos here already on modal & Intuitionistic logic, both of which are intensional. If that’s what you had in mind, have a look at these playlists: Modal Logic ua-cam.com/play/PLwSlKSRwxX0qXTZKnIT7l4_YAIWpJcZJ9.html Intuitionistic logic ua-cam.com/play/PLwSlKSRwxX0pgLLAvnyeppnuFw59Dhuco.html
Great video! I’m glad you’re doing meta logic videos since i’ll be starting a meta logic class next semester. But I have a question, how is that proof meta logical if it uses strategies of logic like universal generalization and universal instantiation?
Metalogic = reasoning about some logic. We can use any kind of good deductive reasoning, including the rules encoded in natural deduction. In general, ND is a great way to learn about reasoning strategies for maths & logic.
That's really helpful, I get a basic understanding of what metalogic is, and I wonder is it possible to define the rules of metalogic rigorously? For, as far as I know, mathematics is based on ZFC-set theory, ZFC is built upon first-order logic, and rules of first-order logic are governed by metalogic. The rules of Matelogic include natural deduction, some set notion, and something hard to tell. It seems to me there is a loop definition since natural deduction is a part of mathematics.
99% of the time, meta-logic proofs involve the basic natural deduction rules (but set out informally in words) and proof by induction. It's rare (for elementary logic classes at least) to appeal to anything more mathematically advanced than that. As for defining the rules rigorously: FOL + set theory will do it. Most are happy to use classical reasoning, even when reasoning about non-classical logics. Some aren't: true die-hard intuitionists (e.g.) will only use intuitionistic reasoning in their meta-logic.
Even before the start of the video I thought about this. I am stopping the video at the moment, but firstly I want to put my thoughts, and then get back to the video. So, I think that to prove logic we have to use logic (or kinda), so there's no way out except for accept the logic. If we deny it, then we can't say whether or not logic is true: we've just stuck within the bad circle of not knowing what to choose and so on. Let's say A is a method to prove logic. If A works, then logic works, if it doesn't work, we should be start looking for another one, and another one, but all of any new methods must be provable, so let's say A, B... and any other methods should be P or provable. So, if A (or anyone else) belongs to P, then it is provable, and we can prove the logic, if it doesn't - we never do it. But it is interesting that P itself means that P is provable, so therefore P is logical. Conclusion: if logic is provable, then logic is logical, and so on - we will get into that circle within logic. If logic can't be proved, we will never know that: so the other option is just left logic be, without being able to say anything about it.
It's different! Logical pluralism is the idea that there's not one true or correct logic: different logics are good for different things, and we don't have to choose between them. Meta-logic, by contrast, is when we reason *about* a given logic.
What's the point of "you can't use logic notation because you are trying to prove facts about that logic itself, so we'll use English" if then you proceed using English with same logical phrases that got formalized as this notation at the first place? Isn't such a way of proof still secretely looping, creating logical proofs about logic using that same logic?
The point is not confusing the object language with the meta language. Of course you use logical rules in proving stuff about logic, because you can’t reason at all without using logic.
hi mate, just wanted to say you single-handedly saved my uni career this last semester and I really appreciate it. thanks so much
Wow, that’s great to hear! I’m still surprised that a few videos can make a difference!
Whenever I get confused in my uni logic studies, I can get clear explanations from your videos, in almost every topic. I love the clear way you explain things, you are my hero.
Aw, thanks! That’s exactly why I set this channel up, so great to hear this!
Aw, thanks! That’s exactly why I set this channel up, so great to hear this!
Amazing, I've been self-teaching myself formal logic for a little under a year and so far this has been more clear and informative an explanation of metalogic, soundness and completeness than what I've attempted to read in 6 intro textbooks and multiple youtube videos. Thank you.
Great to hear! I hear that a lot - often textbooks explain some topics (trees, or whatever) in lots of detail, then go on to prove something about those trees (or whatever) without explaining how those metalogic proofs work.
@@AtticPhilosophy Your videos are to undergrads what Russell's explanations of calculus were to younger Kit Fine. Keep it up! 👌🏻
Awesome! Are there any metalogic text books you recommend?!
Most logic textbooks have some basic metalogic. Richard Jeffrey’s Formal Logic: Scope & Limits is old but excellent, it really simplifies completeness with tree proofs. The standard handbook of advanced results is Boolos & Jeffrey, Computability & Logic.
That particular proof seems very particular to binary systems. Supposes we draw from a sack of random sentences. We know what to do with truths, we keep 2 of them, and with any that evaluate as false we simply discard, but those in a 3rd state, we have no way to decide to keep or discard, so if we draw one from the sack, the procedure is stuck.
Great (and really helpful) explanation as usual. When I first got into contact with metalogic, we just went through the proofs without any backround information and I was really confused about what I was doing. The question I have is can you reason about all different logics the same way ? For example if I have a logic, where proof of contradiction doesn‘t work, can I use an informal version of that proof, when doing metalogic about that logic?
Great question! It really depends. We often reason classically about (e.g.) intuitionism or paraconsistent logic. That's fine if you're just trying to see how they work. It's also by far the easiest way to reason about a logic. But it's obviously not acceptable to committed (e.g.) intuitionists or dialethists. Giving an intuitionistic proof of intuitionistic completeness is much harder, since you have fewer rules to work with & it needs to be constructive. Reasoning about LP using just (extensional) LP would probably be impossible, since then you don't even have modus ponens! (You'd need at least to add a detachable conditional.)
Great video as always! I was wondering, any chance you have or plan to do anything on intensional logic?
Thanks! There’s some videos here already on modal & Intuitionistic logic, both of which are intensional. If that’s what you had in mind, have a look at these playlists: Modal Logic
ua-cam.com/play/PLwSlKSRwxX0qXTZKnIT7l4_YAIWpJcZJ9.html
Intuitionistic logic
ua-cam.com/play/PLwSlKSRwxX0pgLLAvnyeppnuFw59Dhuco.html
Great video! I’m glad you’re doing meta logic videos since i’ll be starting a meta logic class next semester. But I have a question, how is that proof meta logical if it uses strategies of logic like universal generalization and universal instantiation?
Metalogic = reasoning about some logic. We can use any kind of good deductive reasoning, including the rules encoded in natural deduction. In general, ND is a great way to learn about reasoning strategies for maths & logic.
That's really helpful, I get a basic understanding of what metalogic is, and I wonder is it possible to define the rules of metalogic rigorously? For, as far as I know, mathematics is based on ZFC-set theory, ZFC is built upon first-order logic, and rules of first-order logic are governed by metalogic. The rules of Matelogic include natural deduction, some set notion, and something hard to tell. It seems to me there is a loop definition since natural deduction is a part of mathematics.
99% of the time, meta-logic proofs involve the basic natural deduction rules (but set out informally in words) and proof by induction. It's rare (for elementary logic classes at least) to appeal to anything more mathematically advanced than that. As for defining the rules rigorously: FOL + set theory will do it. Most are happy to use classical reasoning, even when reasoning about non-classical logics. Some aren't: true die-hard intuitionists (e.g.) will only use intuitionistic reasoning in their meta-logic.
Even before the start of the video I thought about this. I am stopping the video at the moment, but firstly I want to put my thoughts, and then get back to the video. So, I think that to prove logic we have to use logic (or kinda), so there's no way out except for accept the logic. If we deny it, then we can't say whether or not logic is true: we've just stuck within the bad circle of not knowing what to choose and so on.
Let's say A is a method to prove logic. If A works, then logic works, if it doesn't work, we should be start looking for another one, and another one, but all of any new methods must be provable, so let's say A, B... and any other methods should be P or provable. So, if A (or anyone else) belongs to P, then it is provable, and we can prove the logic, if it doesn't - we never do it. But it is interesting that P itself means that P is provable, so therefore P is logical.
Conclusion: if logic is provable, then logic is logical, and so on - we will get into that circle within logic.
If logic can't be proved, we will never know that: so the other option is just left logic be, without being able to say anything about it.
Great content! I have a question though !!
Can we define interfaces in meta logic ?
Hi, not sure what you mean by interfaces!
@@AtticPhilosophy Like an interface between two different things. Do we have this in meta logic ? Or Meta logic is itself an interface ??
Is this different to logical pluralism? Thanks for the video ❤️🔥
Can this be related to pluralism rather?
It's different! Logical pluralism is the idea that there's not one true or correct logic: different logics are good for different things, and we don't have to choose between them. Meta-logic, by contrast, is when we reason *about* a given logic.
Attic has a double meaning here because Attica is the historical region containing Athens where Aristotle invented formal logic.
At last, someone gets it!
What's the point of "you can't use logic notation because you are trying to prove facts about that logic itself, so we'll use English" if then you proceed using English with same logical phrases that got formalized as this notation at the first place? Isn't such a way of proof still secretely looping, creating logical proofs about logic using that same logic?
The point is not confusing the object language with the meta language. Of course you use logical rules in proving stuff about logic, because you can’t reason at all without using logic.
metalogic perfectly explain why the earth is flat...