0
$\begingroup$

$\DeclareMathOperator\Cn{Cn}\DeclareMathOperator\Sb{Sb}$I would like to ask about the Deduction Theorem for an inconsistent system. This is a very well-known fact that for the classical propositional calculus, the classical Deduction Theorem (proved independently by Tarski and Herbrand), in the case of the classical propositional calculus, holds only for the invariant form of this calculus (I cite here a fragment of: Witold A. Pogorzelski, "The Classical Propositional Calculus", PWN, Warszawa 1975): $$\Psi \in \Cn(R_{0}, \Sb(A_{2}) \cup X \cup {\Phi}) \Rightarrow (\Phi \rightarrow \Psi) \in \Cn(R_{0}, \Sb(A_{2}) \cup X),$$

where $\Cn$ is the very well-known consequence operation, $\Sb(A_{2})$ is the set of all substitutions of the formulas belonging to $A_{2}$ by the formulas belonging to the set of all well-formed formulas $S_{2}$, and $X$ is any subset of $S_{2}$ and $\Phi, \Psi \in S_{2}$. $A_{2}$ is the set of all axioms of the classical propositional calculus. $r_{0}$ is the detachment rule and $R_{0}=\{r_{0}\}$. As this is also very well-known fact, the Deduction Theorem does not hold for consistent system, where besides the detachment rule, we have also substitution rule (in the set of all inference rules).

On the other hand, there are also the so-called indirect Deduction Theorems (proved by Stan J. Surma). One of the exercises in Pogorzelski's handbook concerns proving that for the implicational-negational system, the following form of the indirect Deduction Theorem, holds: $\Phi, \mathord\sim \Phi \in \Cn(R, A \cup X \cup \{\Psi, \mathord\sim \Gamma \}) \Rightarrow (\Psi \rightarrow \Gamma) \in \Cn(R, A \cup X)$. This exercise concerns also proving that from this above formula follows also the following: $\forall X \subseteq S_{2} \ \ \forall \Phi,\Psi \in S_{2} \ [ \Psi \in \Cn(R, A \cup X \cup \{\Phi \}) \Rightarrow (\Phi \rightarrow \Psi) \in \Cn(R, A \cup X)]$, without any assumptions concerning the set of inference rules $R$ and the set $A$ i.e. in the case of inconsistent system, the Deduction Theorem is valid also, when the substitution rule is among the inference rules.

My question is, whether anybody knows, in which paper (or book) is a proof of the above form of the indirect Deduction Theorem ? A note: "S. J. Surma", placed in the text of this exercise, suggests that such proof is in one of the papers of Stan J. Surma, however I have not found this proof in any paper of Stan J. Surma, as yet.

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Commented Sep 27 at 6:37
  • $\begingroup$ @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 $\endgroup$
    – Luke
    Commented Sep 27 at 11:04
  • $\begingroup$ 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 $\endgroup$
    – Luke
    Commented Sep 27 at 13:44
  • $\begingroup$ This definitely looks like an AI generated question. $\endgroup$
    – coudy
    Commented Sep 27 at 14:00
  • $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Commented Sep 27 at 16:58

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .