The Deduction Theorem | MetaLogic | Attic Philosophy

The deduction theorem links logical entailment to implication (if … then). It says that A entails B just in case the sentence ‘if A then B’ is valid. This is a central principle of almost all logics. In this video, we look at what the deduction theorem means, why it’s important, and how we can prove it.

00:00 - Intro
00:59 - The Deduction Theorem
02:48 - A bit like Conditional Proof
03:33 - Proving the Deduction Theorem
05:56 - Recap of proof left-to-right
06:15 - Proof right-to-left
08:16 - In other logics
09:17 - Wrap up

If there’s a topic you’d like to see covered, leave me a comment below.

Links:

Get in touch on Social media!

#logic #philosophy

[Red_]

Going to binge all your logic videos so I can cram all the info and hopefully pass my logic final in 2 weeks 🤞

[vitusschafftlein]

As always, great video! I have some questions:
1. Obviously, the conditional introduction rule I→ is closely connected to the deduction theorem. But can you go so far as to say that for any logic, the deduction theorem holds iff I→ is a rule of its natural deduction system, or at least derivable in it?
2. Follow up to 1.: Is it even possible to derive that rule by intelligently choosing your deduction rules or do you need it as a primitive rule?
3. Let Γ be an arbitrary set of formulas. As far as I see it, you only prove a special instance of the deduction theorem, namely the one for |Γ|=1. I think it does not account for two important cases. Firstly, the case where |Γ|>1 but Γ is finite. Secondly, the case where |Γ|=|ℕ|. Am I missing a link? If not, does the proof with Γ instead of A differ from the one you gave?
4. The way you use the whiteboard is awesome! Which one do you use?

If you're thinking about doing some more metalogic, I would love to see a consistency proof for propositional logic!

[karlnauman]

In the context of relevance logic, can the deduction theorem be false?

[ostihpem]

So the semantic deduction theorem, i.e. {A1, …, An} |= B iff |= A1, …, An -> B, does also hold in Modal Logic (of course not globally but just for a particular model)?