Return to Question

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, \sim \Phi \in Cn(R, A \cup X \cup \{\Psi, \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.

$\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.

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 concern proving that for the implicational-negational system, the following form of the indirect Deduction Theorem, holds: $\Phi, \sim \Phi \in Cn(R, A \cup X \cup \{\Psi, \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.

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, \sim \Phi \in Cn(R, A \cup X \cup \{\Psi, \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.