I'm gonna prove if $x$ is not free in $\psi$, then $(\phi \rightarrow \psi)\models (\exists x \phi \rightarrow \psi) $.

Here is my argument:

According to definition of rule of inference of QR, if $x$ is free, then one can deduce $(\exists x \phi \rightarrow \psi)$ from $\phi \rightarrow \psi$. Mathematically: $(\phi \rightarrow \psi)\vdash (\exists x \phi \rightarrow \psi) $. Furthermore, from soundness theorem, we know that, if $a \vdash b$ then $a \models b$. So, according to truth of $(\phi \rightarrow \psi)\vdash (\exists x \phi \rightarrow \psi) $, $(\phi \rightarrow \psi)\models (\exists x \phi \rightarrow \psi) $ holds.

Is this sort of argument valid?

If one says (you must prove that "if $x$ is free, then one can deduce $(\exists x \phi \rightarrow \psi)$ from $\phi \rightarrow \psi$", I don't know the argument for that.)


$(\phi \rightarrow \psi) \models (\exists x \phi \rightarrow \psi)$

$(\phi \rightarrow \psi) \models \neg(\exists x \phi) \vee \psi$

$(\phi \rightarrow \psi) \models (\forall x (\neg \phi)) \vee \psi$

$(\neg\phi \vee \psi) \models (\forall x (\neg \phi)) \vee \psi$

$(\neg\phi \vee \psi) \models (\forall x (\neg \phi)) \vee \psi$

By universal instantiation:

$(\neg\phi \vee \psi) \models (\neg \phi) \vee \psi$

Which is true.

enter image description here

  • $\begingroup$ What is QR? Also, did you mean to say that $x$ is not free in $\phi$? $\endgroup$ – Bram28 Jan 25 '17 at 1:44
  • $\begingroup$ @Bram28; Please find the update. $\endgroup$ – Roboticist Jan 25 '17 at 1:53
  • $\begingroup$ I do not think that it works... The soundness theorem relies on the soundness of the rules. Thus, you have to show that the rule is sound according to the semantical specifications of the system. $\endgroup$ – Mauro ALLEGRANZA Jan 25 '17 at 8:13
  • $\begingroup$ @Roboticist Can you please post that picture of the problem statement that you had up yesterday? Thanks! $\endgroup$ – Bram28 Jan 25 '17 at 15:15
  • 1
    $\begingroup$ @Roboticist Thanks! So, if you follow the discussion I had with Mauro, you'll see that I had this wrong: depending on how exactly you define the semantics, apparently it is ok for $\phi$ to have $x$ as a free variable! And, unless you have a proof system with inference rules that allow free variables, that means you really need to take that semantical approach to prove what you want ... which is exactly what Mauro did. $\endgroup$ – Bram28 Jan 25 '17 at 19:05


See Ch.2.5 Soundness : our rules of inference will preserve truth, i.e. for a rule $⟨Γ,θ⟩ : Γ⊨θ$.

And see Th.2.5.2 for the proof that the rules are sound.

The Exercise asks to prove that the second QR rule :

$\langle \{ \phi \to \psi \} , (\exists x) \phi) \to \psi \rangle$, $x$ not free in $\psi$,

preserves truth.

Assume a structure $\mathfrak A$ such that $\mathfrak A \vDash (\phi \to \psi )$, i.e. for any assignment function $s$ : $\mathfrak A \vDash (\phi \to \psi )[s]$.

We have to prove that : $\mathfrak A \vDash ((\exists x)\phi \to \psi )[s']$, for every $s'$.

Case (i) : If $\mathfrak A \vDash \psi[s']$, it's done.

Thus, consider :

Case (ii) : $\mathfrak A \nvDash \psi[s']$.

We want that $\mathfrak A \nvDash (\exists x)\phi[s']$, i.e. that $\mathfrak A \nvDash \phi[s'[x|a]]$ for some $a \in \text {dom}(\mathfrak A)$.

But we know that : $\mathfrak A \vDash (\phi \to \psi )[s]$ for every $s$, and thus also : $\mathfrak A \vDash (\phi \to \psi )[s'[x|a]]$.

But $x$ is not free in $\psi$ and thus $s'$ and $s'[x|a]$ agree on the free variables of $\psi$; thus, from $\mathfrak A \nvDash \psi[s']$ we have also : $\mathfrak A \nvDash \psi[s'[x|a]]$, for some $a$.

This, due to $\mathfrak A \vDash (\phi \to \psi )[s'[x|a]]$ above, implies that : $\mathfrak A \nvDash \phi[s'[x|a]]$, for some $a$, i.e.:

$\mathfrak A \nvDash (\exists x)\phi[s']$.


So two things:

First, you are trying to prove that this logical entailment holds on the basis of an existing inference rule plus soundness. OK, that should work ... If you know that this specific inference rule is sound. Do you know that? I mean, yes, there are many sound systems of logic (indeed, presumably most systems of logic are sound) .. But just because we are presented with some system and some inference rule doesn't mean it is sound; we would have to prove that it is sound, which means we would need to prove exactly the entailment you want to prove. So unless someone told you that this specific inference rule is sound, this would become a circular argument. Indeed, I suspect that the whole goal of the exercise you are presented with is to prove the very soundness of this very inference rule, meaning that your approach would indeed be circular (you'd assume the proof system that includes this inference is sound in order to prove that this inference rule is sound). So, you most likely need to use formal semantics to prove this.

Second, about the actual soundness of this inference rule (or the validity of the entailment) ... I must say it looks very weird: it says that $x$ is not free in $\psi$ .. But the inference rule really doesn't do anything with $\psi$; instead, it quantifies the $\phi$. Meaning that if $x$ is a free variable in $\phi$, then we have a big problem since that would mean that we have a different set of variables free between the left hand side and the right hand side... in a way, we would be comparing apples with oranges! So, I think a mistake was made here, and that they should have said that $x$ is not a free variable in $\phi$ .. And then the entailment actually holds!


OK, so I had this last part wrong: with a proper semantics, you can make sense of (and prove!) $\phi \rightarrow \psi \vDash \exists x \phi \rightarrow \psi$, even if $\phi$ contains free variables (see Mauro's answer).

  • $\begingroup$ To get rid of such circulation, how should I prove that inference rule is sound?... $\endgroup$ – Roboticist Jan 25 '17 at 2:57
  • $\begingroup$ @Roboticist You will need to go into formal semantics, considering what it takes for an interpretation to set some statement to true. Logical entailment means that for all interpretations that set the implying statement(s) to true, they will set the implying statement to true as well. $\endgroup$ – Bram28 Jan 25 '17 at 3:03
  • $\begingroup$ Could you please see UPDATE 2?... I hope I'd just solved the issue without the circulation. $\endgroup$ – Roboticist Jan 25 '17 at 3:44
  • $\begingroup$ But you are starting with what you are trying to prove ... $\endgroup$ – Bram28 Jan 25 '17 at 4:25
  • 1
    $\begingroup$ And you said the approach is not so reliable... Now, I'm trying to find a right one, based on your signal. $\endgroup$ – Roboticist Jan 25 '17 at 4:27

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.