Timeline for the (indirect) deduction theorem
Current License: CC BY-SA 4.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 27 at 16:58 | comment | added | Emil Jeřábek | Since the moderator who converted the beginnings of the now deleted answers to the comments above did not transfer my comments as well, I repeat: if you allow substitution in $R$, the claim in your question, namely $\Phi, {\sim} \Phi \in \mathrm{Cn}(R, A \cup X \cup \{\Psi, {\sim}\Gamma \}) \implies(\Psi \to \Gamma) \in \mathrm{Cn}(R, A \cup X)$, fails e.g. when $A=X=\varnothing$, $Ψ=Φ=p$, $Γ=q$ (where $p$ and $q$ are propositional atoms). This is just a minimal example; it can be varied in all kinds of ways. | |
| Sep 27 at 14:00 | comment | added | coudy | This definitely looks like an AI generated question. | |
| Sep 27 at 13:44 | comment | converted from answer | Luke | This can be considered as my comment to my first post. Namely, Surma had written in the chapter "Deduction Theorem" in "Dictionary of Logic", Springer Science+Business Media Dordrecht 1981 (W. Marciszewski (editor)): > Nevertheless sometimes the theorem is stated for the propositional calculus with a restricted substitution, i.e., the substitution restricted to the propositional variables which occur in no hypotheses of a formalized proof under consideration. > So, this, the fragment of Pogorzelski's handbook cited by me, and Surma's paper on the indirect Deduction Theorems, cited by me prev | |
| Sep 27 at 13:12 | review | Close votes | |||
| Oct 4 at 3:22 | |||||
| Sep 27 at 11:23 | history | edited | LSpice | CC BY-SA 4.0 |
TeX
|
| Sep 27 at 11:04 | comment | converted from answer | Luke | @Emil Jerabek. Thank you for your answer. As a comment to your answer, I write that I have checked exactly my post in comparison with Pogorzelski's handbook and everything is OK. I give here an exact quote from a chapter of this handbook, devoted to the Classical Deduction Theorem. Namely, it seems that he highlights the issue exactly > for any consistent i.e. such that its set of consequences $\neq S$ - system $\langle R, A\rangle$, in which $R_{0\ast} \subseteq \operatorname{Der}(R,A)$, one cannot prove the Classical Deduction Theorem. > whe | |
| Sep 27 at 6:37 | comment | added | Emil Jeřábek | I have a hard time deciphering the question and the notation. But as far as I can see, none of the above-mentioned versions of the deduction theorem hold if you allow freely to use the substitution rule. Thus, you are likely misinterpreting something. | |
| Sep 27 at 6:30 | history | edited | Emil Jeřábek |
edited tags
|
|
| Sep 26 at 22:55 | history | edited | Luke | CC BY-SA 4.0 |
added 1 character in body
|
| Sep 26 at 22:55 | history | edited | Luke |
edited tags
|
|
| Sep 26 at 22:52 | history | edited | Luke | CC BY-SA 4.0 |
added 31 characters in body
|
| Sep 26 at 22:51 | history | edited | Luke | CC BY-SA 4.0 |
deleted 1 character in body
|
| Sep 26 at 22:50 | history | edited | Luke | CC BY-SA 4.0 |
deleted 12 characters in body
|
| S Sep 26 at 22:49 | review | First questions | |||
| Sep 27 at 0:44 | |||||
| S Sep 26 at 22:49 | history | asked | Luke | CC BY-SA 4.0 |