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] = (A \rightarrow B) \rightarrow A$ and letting $x_2[A, B] = A)$, it is necessarily true that $\vdash ((A \rightarrow B) \rightarrow A) \implies \vdash A$, but it is not necessarily true that $\vdash ((A \rightarrow B) \rightarrow A) \rightarrow A$.

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

Note: The original version of this question did not use the correct notation, resulting in entirely different semantics, so I created this new question based on guidance I received from this meta question. Many thanks to @Hurkyl and @HenningMakholm for helping me to get the notation right.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.