What is this property relating to logical systems called?

This is called the deduction-resolution property; it's probably best to think of it as $$\Gamma,\alpha \vdash \beta \iff \Gamma \vdash \alpha \rightarrow \beta.$$

Under the usual way of thinking about things, first-order logic does have this property, but we assume that $\alpha$ is a sentence, not just a formula.

It's worth noting the close relationship to the lattice-theoretic perspective on implication, in which the formula $$a \wedge b \leq c \iff a \leq b \rightarrow c$$ defines logical implication, also known as "relative pseudocomplements", also known as "exponential objects." See here, for example.

Note also the connection to Cartesian closed categories, closed monoidal categories, and closed multicategories. The latter categorify the deduction-resolution property to give a notion of internal homs with possibly-multiple arguments.


This is called the deduction theorem. Yes, it holds in classical propositional logic and it does hold in classical logic, provided that either you restrict it to conditionals with closed antecedents (thus blocking the problematic inference involving a formula with free variables in the antecedent) or you restrict the universal generalization rule (Jeffrey Ketland has some interesting remarks on the options in this blog post; check out the article linked in his post).