# What is this property exhibited by some logical systems?

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:

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.)

• Can $x_1, x_2$ contain fixed variables ? As in $x_1[A] = A\implies B$ ? – Max Mar 5 '18 at 7:06
• @Max no. But you could do $x_1[A, B] = A$ and $x_2[A, B] = B$ – Hans Brende Mar 5 '18 at 7:12
• While intuitionistic logic, indeed, does not have the property, the argument in the question is wrong: for example, taking $\neg\neg p\to p$ for $A$, and $\neg p$ for $B$, we have $\vdash(A\to B)\to A$, but $\nvdash A$. – Emil Jeřábek Mar 5 '18 at 7:58
• Your example does not work for minimal logic either, just take $A=(((p\to q)\to p)\to p)$, $B=(p\to q)$. Well-known rules admissible but not derivable in intuitionistic logic include the independence of premise (aka Harrop's) rule $\vdash\neg A\to B\lor C\implies\vdash(\neg A\to B)\lor(\neg A\to C)$, the Scott rule $\vdash(\neg\neg A\to A)\to A\lor\neg A\implies\vdash\neg\neg A\lor\neg A$, or Mints's rule $\vdash(A\to B)\to A\lor C\implies\vdash((A\to B)\to A)\lor((A\to B)\to C)$. The more general Visser's rules are, I believe, mentioned on the Wikipedia page I linked from my answer. – Emil Jeřábek Mar 5 '18 at 9:56
• No, for instance the Mints or Visser rules are also admissible in minimal logic. (In general, it holds that a rule expressed using only positive connectives is admissible in minimal logic if and only if it is admissible in intuitionistic logic.) – Emil Jeřábek Mar 5 '18 at 11:56

• I can’t think of any implications for other properties of the logic. Concerning predicate logics: it may depend on how you define “predicate logic” (I am going to assume it is at least closed under formula substitution), but no, not really, if you stick to reasonable logics that would appear in the literature. For an example of what can go wrong, consider the formula $A=\exists x\,\exists y\,(P(x)\land\neg P(y))$. There are two possibilities: (1) No instance of $A$ is provable. Then by structural completeness, $\neg A$ is provable, hence so are all its instances. Since this amounts to all ... – Emil Jeřábek Mar 6 '18 at 14:31
• ... individuals having the same properties, this is effectively a propositional logic, the quantifiers are redundant. (2) Some instance $A'=\sigma(A)$ of $A$ is provable. Thus, the logic itself proves that there exist at least two elements distinguished by their properties. But what’s more, the logic has to prove all instances of $A'$ as well, even if, for example, we substitute all predicates in $A'$ with a trivially true formula! It is not really possible for a formula of this form to have different truth values for different elements, thus the logic is really inconsistent. ... – Emil Jeřábek Mar 6 '18 at 14:37
• ... But maybe the logic includes “logical predicates” such as $x=y$, that cannot be substituted? Well, then let $A$ be the sentence using just $=$ which says that the universe has at least $42$ elements. Again, either $A$ is provable, or, by structural completeness, $\neg A$ is provable. This can be of course done for all finite numbers, not just $42$, Thus, either there is a fixed integer $k$ such that the logic proves that all models have exactly $k$ elements, or it proves that all models are infinite. In the latter case, the fun continues. Let $A$ be a sentence expressing ... – Emil Jeřábek Mar 6 '18 at 14:41
• ... a nontrivial theory, such as the conjunction of axioms of dense linear orders, or of Robinson arithmetic. Again, either (1) the logic proves an instance of $A$, or (2) it proves $\neg A$. In case (1), it means the logic has to somehow have a built-in dense order, or arithmetic, or whatever, in such a way that it cannot be substituted away. In case (2), the logic proves that no such thing as a dense linear order can be definable in any model. Neither of these possibilities is remotely reasonable for a “logic”. – Emil Jeřábek Mar 6 '18 at 14:45