Necessary and sufficient conditions on antecedent for deduction theorem

95 Views Asked by At

The deduction theorem for classical predicate logic states that for any set of wffs $\Gamma$ , any closed wff $A$, and any wff B, if $\Gamma\cup\{A\}\vdash B$, then $\Gamma\vdash A\implies B$. The condition that $A$ is closed is sufficient, but it is clearly not necessary, i.e., there are wffs with free variables that satisfy the deduction theorem. Are there any known necessary and sufficient conditions on $A$ for the deduction theorem? If not, what are strongest known conditions on $A$?

Here are some definitions: Let $\Sigma$ be a complete and consistent set of axioms/inference rules for predicate calculus. For any set of wffs $\Gamma$, and any wff $A$, we say that $\Gamma\vdash A$ iff there exists a deduction from $\Sigma\cup\Gamma$ to $A$. Additionally, we say that $\Gamma\vDash A$ iff for every interpretation $\mathcal{M}$ and valuation $v$, if $\mathcal{M},v\vDash\Gamma$ then $\mathcal{M},v\vDash A$.