I'm migrating this question from MSE to MO, as in the span of five months, it received 6 upvotes but no answers. If my language needs to be fine-tuned in any way, constructive suggestions and guidance would be greatly appreciated.

The following property exhibited by some logical systems has captured my attention:

$$\forall X\; ( {\vdash x_1[X]} \implies {\vdash x_2[X]} ) \implies \forall X\; {\vdash (x_1[X]\to x_2[X])},$$

where $X$ ranges over "ways to fill in the holes in $x_1$ and $x_2$", for any syntactically correct schemas $x_1$ and $x_2$.

In other words, the property states that if $x_2[X]$ is provable whenever $x_1[X]$ is provable, then all instances of the schema ($x_1 \rightarrow x_2$) are also provable.

Some examples off the top of my head of where this property *does not* hold:

- Classical predicate logic
*does not*have this property because (letting $x_1[P] = P$ and letting $x_2[P] = \forall x.P$), it is necessarily true that $(\vdash P) \implies (\vdash \forall x.P)$, but it is*not*necessarily true that $\vdash (P \rightarrow \forall x.P)$ - Intuitionistic logic
*does not*have this property because (letting $x_1[A, B, C] = \neg A\to B\lor C$ and letting $x_2[A, B, C] = (\neg A\to B)\lor(\neg A\to C))$, it is necessarily true that $(\vdash\neg A\to B\lor C)\implies(\vdash(\neg A\to B)\lor(\neg A\to C))$, but it is*not*necessarily true that $\vdash(\neg A\to B\lor C)\rightarrow((\neg A\to B)\lor(\neg A\to C))$.

My question is 3-fold:

- Does this property have a name? If so, what is it called?
- Does classical
*propositional*logic have this property? (I'm assuming it does, but I want to be sure.) What other systems display this property? - Does the presence of this property (or lack thereof) imply any other important properties about the system in question? (I realize that this third part of the question might seem overly broad, but what I really want to know is: is this property
*important*and if so,*why*? Deep insights appreciated.)

Partial answers welcomed as well.