I'm migrating [this question from MSE](https://math.stackexchange.com/questions/2420887/what-is-this-property-exhibited-by-some-logical-systems) 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: 


1. Does this property have a name? If so, what is it called?
2. Does classical *propositional* logic have this property? (I'm assuming it does, but I want to be sure.) What other systems display this property?
3. 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.



What is this property exhibited by some logical systems?
This is equivalent to a combination of *structual completeness* with the *deduction theorem*. For a start, see [Wikipedia](https://en.wikipedia.org/wiki/Admissible_rule).


