A deduction theorem schema for deductive systems of propositional logics (Q1189891)

The authors propose a new schema for a deduction theorem for propositional logics. They prove that the logic \(L\) fulfills the schema if and only if there exists a finite set \(A(p,q)\) of propositional formulas involving only \(p\), \(q\) such that \(\vdash A(p,p)\) and \(p,A(p,q)\vdash q\) for each \(A(p,q)\). The new schema is defined in terms of a family \(F\) of finite sets of propositional formulas involving \(p\), \(q\) and perhaps other propositional letters, a set of formulas \(X\), single formulas \(A\), \(B\), and a sequence of propositional formulas \(s\). The schema is \(X,A\vdash B\) iff there exists \(P\) in \(F\) and a sequence \(s\) of appropriate length such that \(X\vdash P(p/A,q/B,s),P(p/A,q/B,s)\) is the result of simultaneously substituting in all formulas of \(P\), \(A\) for \(p\), \(B\) for \(q\) and the elements of \(s\) for propositional letters of \(P\) other than \(p\), \(q\). In addition to proving their theorem they illustrate application of the schema to familiar deduction theorems.