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!
Thanks! Arrow-intro gets you one direction: from A |- B to |- A>B. The other direction is basically modus ponens. I suppose you could have other intro rules for arrow, like introducing from either ~A or from B, but only classically for the material arrow. Arrow-intro does a much better job of capturing what the arrow means. Or you could have just elimination rules, one for arrow on the left and one for it on the right of the turnstile, like in a sequent system. But if you want an intro and an elim rule for each symbol, arrow-intro is the natural choice. In most systems, finite sets of premises can be reduced to the single-premise case with conjunction: A1 … An |- C iff A1 & … & An |- C.
And the whiteboard: that’s writing on an iPad, recording the screen, then importing into final cut. I found writing in white on a plain black background made it easiest. I add the blackboard image (a photo from my old office!) in final cut, so the white writing shows over the top (‘screen’ compositing mode).
Yes, it doesn’t hold in the presence of conjunction. In relevance logic, “positive paradox”, A > (B > A) isn’t valid, but it can be derived from the deduction theorem via residuation, like this. First, A&B |- A. Residuation transforms this to A |- B > A and so, if we had the deduction theorem, we could infer |- A > (B > A).
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)?
Yes, it holds in modal logic, because propositional logic holds at each world. So anywhere where the premises are true, their conjunction is also true, and if B follows, then any world will support the corresponding material implication.
@@AtticPhilosophy Thanks a lot. Just to be deadsure: The semantic deduction theorem is always bound to a certain model and a certain (local) world, so one would need to write it down in Modal Logic for instance for a model T: V(w_i) {A1, …, An} |= V(w_i) B iff |= V(w_i) A1, …, An -> B, right? Or would you also say the deduction theorem holds globally within a model?
@@ostihpem entailment is defined as preservation of truth relative to all worlds in all models. So it’s simply a statement about premises entailing a conclusion - no need to mention models or worlds.
