7
$\begingroup$

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

Partial answers welcomed as well.

Improve this question
$\endgroup$
11
  • $\begingroup$ Can $x_1, x_2$ contain fixed variables ? As in $x_1[A] = A\implies B$ ? $\endgroup$
    – Maxime Ramzi
    Commented Mar 5, 2018 at 7:06
  • $\begingroup$ @Max no. But you could do $x_1[A, B] = A$ and $x_2[A, B] = B$ $\endgroup$
    – Hans Brende
    Commented Mar 5, 2018 at 7:12
  • 2
    $\begingroup$ 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$. $\endgroup$
    – Emil Jeřábek
    Commented Mar 5, 2018 at 7:58
  • 1
    $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Commented Mar 5, 2018 at 9:56
  • 1
    $\begingroup$ 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.) $\endgroup$
    – Emil Jeřábek
    Commented Mar 5, 2018 at 11:56

1 Answer 1

Reset to default
11
$\begingroup$

This is equivalent to a combination of structual completeness with the deduction theorem. For a start, see Wikipedia.

Improve this answer
$\endgroup$
5
  • $\begingroup$ The information contained in this answer and your comments above is, I repeat, gold. I've been pouring over the wikipedia article, but one thing it doesn't seem to touch on too much is part 3 of my question: the implications of structural completeness. Aside from the inherent beauty evident to me in such a system that, in a sense, perfectly describes itself, are there other advantages inherent in such a system? Theorems? Connections to other concepts (e.g. Gödel completeness)? I want to know why this property mesmerizes me :) Also, are there structurally complete predicate logics? $\endgroup$
    – Hans Brende
    Commented Mar 6, 2018 at 6:12
  • 2
    $\begingroup$ 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 ... $\endgroup$
    – Emil Jeřábek
    Commented Mar 6, 2018 at 14:31
  • 1
    $\begingroup$ ... 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. ... $\endgroup$
    – Emil Jeřábek
    Commented Mar 6, 2018 at 14:37
  • 1
    $\begingroup$ ... 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 ... $\endgroup$
    – Emil Jeřábek
    Commented Mar 6, 2018 at 14:41
  • 1
    $\begingroup$ ... 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”. $\endgroup$
    – Emil Jeřábek
    Commented Mar 6, 2018 at 14:45

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .