4
$\begingroup$

Doing some homework, I'm asked to determine if the following formula is satisfiable, valid or neither.

I am confused by the nesting quantifiers for the same variables.

Using sequent calculus, I derive this is not valid, but I think it's valid because the variables are all bounded to the same first quantifier.

$$\exists x\exists y (P (x, y) \rightarrow \forall x\forall y P (x, y))$$

Help would be much appreciated.

Edited to avoid confusion. This is about classical FOL using sequent calculus.

  • 0
    Do you mean $\exists x\exists y\ldots \forall x\forall y\ldots $?2011-10-24
  • 0
    Yes, where ∀x∀y are inside the scope of ∃x∃y, ie ∃x∃y(...∀x∀y(...)).2011-10-24
  • 0
    The variable bound by a quantifier is completely separate from other uses of the variable letter outside the scope of the quantifier, so your formula is nothing more nor less than $\exists x\exists y.(P(x,y)\to\forall z\forall w. P(z,w))$. This is classically valid, by the way.2011-10-24
  • 0
    @HenningMakholm OK, that change of letters make sense. However, I fail to proof its validity. It's hard for me to type my sequent calculus "proof" (it's: $\exists right; \rightarrow right; \forall right$ and then I end up with different variables on each side). Thanks for the comment :)2011-10-24
  • 0
    Hint: since it's classically valid _but not intuitionistically valid_, you'll need to use sequents with more than one formula on the right-hand side. It may be easier to draft the proof as $\exists x.(\phi(x)\to\forall y.\phi(y))$ and then double the variables afterwards.2011-10-25
  • 0
    @HenningMakholm $$ P(x) \Rightarrow P(y)) $$ $$___________________$$ $$ P(x) \Rightarrow \forall y P(y) $$ $$___________________$$ $$ \Rightarrow P(x) \rightarrow \forall y P(y) $$ $$___________________$$ $$\Rightarrow \exists x (P(x) \rightarrow \forall y P(y)) $$ I hope it's clear what I've done in each step (I know, I suck at LaTeX). In the last step (top one) I can't instantiate $y$ to $x$ because $x$ is free in the LHS), so I don't know where to go from there. Note the double right arrow is sometimes replaced by a turnstile in sequent calculus.2011-10-25
  • 0
    It's been too long since I did real work with sequents, but I doubt eliminating the quantifiers in this way will be productive. My suggestion would be to prove $\forall yP(y)\lor\neg\forall yP(y)$ separately using a standard skeleton for excluded middle; then cut it over to the LHS and then split on it with rule $L{\lor}$. In the $\forall yP(y)$ branch you already have the required conclusion, and in the $\neg\forall yP(y)$ branch you can prove $\exists x.\neg P(x)$ and use proof by contradiction under the $\exists$.2011-10-25
  • 0
    @HenningMakholm those are the rules we have been taught so far. I'll look into that method as well. Thank you.2011-10-25
  • 0
    I always use this formula $\exists ( P(x) \to \forall y P(y))$ when teaching logic. It does a great job with students if you use the following interpretation of the predicate $P$: "student that will pass the exams". In other words, in this context the sentence $\exists ( P(x) \to \forall y P(y))$ says that: "there is some student such that if he passes the exams, then everybody pass the exams".2011-10-25
  • 0
    @boumol thanks for the help. How can such a statement be valid? Would that "student" be the one who studies the least, so that his passing implies everyone passes?2011-10-25
  • 0
    @user18180: Your answer is right, it is enough to consider the student with the smallest score. This student is a witness of the validity of this existential. By the way, the formula I wanted to write is $\exists x (P(x) \to \forall y P(y))$ (somehow I forgot the $x$ in the existential).2011-10-25
  • 0
    @user18180 Notice that you can vote on the answers, just as we can vote on the questions.2011-10-25
  • 0
    @MichaelHardy Yes, but I still don't have enough reputation to do so. I'd up voted the answers if I could :)2011-10-25
  • 0
    @boumol how can I prove this with sequent calculus?2011-10-25
  • 0
    @user18180: I will just give you a hint. Use that in classical logic you can prove the sequent "$\Rightarrow \exists x \neg Px, \forall y Py$".2011-10-25

2 Answers 2

2

This is really about how you evaluate the truth value.

$\exists x\varphi(t)$ is true if and only if there exists some $x$ for which $\varphi(x)$ is true. Conversely it is false if and only if for all $x$ (in a given model, of course) $\varphi(x)$ is false.

The inner quantification is mostly to "confuse" your intuition and since the truth value of $\forall x\forall y(P(x,y))$ is not dependent of the truth value of the outer quantification it is easier to change the variables, even informally before writing the actual proof.

The claim itself just says that there is a pair $(x,y)$ such that if $P(x,y)$ then $P$ is all the ordered pairs of the universe.


We can prove the validity of this formula from an external point of view, and we do that semantically (that is we do not try to write a proof, but rather show that is holds in every model), for brevity denote our formula $\varphi$.

Let $M$ be an arbitrary model of our language (where $P$ is a binary relation).

If $M\models\forall x\forall y(P(x,y))$ then $M\models\varphi$ (can you see why?)

If $M\models\lnot(\forall x\forall y(P(x,y))$ then for some $a,b\in|M|$ we have $\lnot P(a,b)$. In particular for this pair that $M\models P(a,b)\rightarrow\forall x\forall y(P(x,y))$, so we have $M\models\varphi$.

If needed, this should be made rigorously using the $\operatorname{val}$ function. I strongly recommend on working the details yourself and following closely after the definitions of $\operatorname{val}_M(\exists x\varphi,g)$ (and similarly $\forall x\varphi$).

  • 0
    This answer makes complete sense. I also understand the last sentence. And my intuition says it's satisfiable (make $P(x,y)$ false for a pair of values and the formula would be true). However, I can't see how that statement would be valid (true in all interpretations).2011-10-25
  • 0
    @user18180: I am not sure what is the framework in which you work here.2011-10-25
  • 0
    Well, an implication is true if the LHS is false, thereby making the whole formula true. Am I incorrect?2011-10-25
  • 0
    @user18180: Yes, you are correct. If there is a pair for which the LHS is false then the formula is true, if there is none then for every pair it is true and the RHS of the implication is true.2011-10-25
  • 0
    @user18180: Of course this is true if you are working in classical FOL, which is why I asked about the framework. The comments on the main question seemed to possibly imply otherwise.2011-10-25
  • 0
    Are these facts of any help to proof the (in)validity of this formula? I think the "obvious" way to prove it is with sequent calculus (it might seem I'm in love with it, so many times I've mentioned it). A failed attempt can be found in a comment to the question.2011-10-25
  • 0
    OK, I see my use of the word intuition might be confusing. Yes, this is classical FOL.2011-10-25
  • 0
    Thank you very much for the added part. I haven't seen the val function yet (this is an introductory class to logic), but I will look into it. Thanks again2011-10-25
  • 0
    @user18180: In the introductory course here we use mostly val for truth definitions. It's tedious and a lot the fault of two mathematicians I highly appreciate otherwise. I really have no idea how one introduces this naively, so I can't give another approach.2011-10-25
2

$$\exists x\;\exists y\; \left(P (x, y) \rightarrow \forall x\;\forall y \;P (x, y)\right).$$

I wonder if the notion of an "alphabetic variant" can make this clearer: $$\exists x\;\exists y\; \left(P (x, y) \rightarrow \forall u\;\forall v \;P (u, v)\right).$$ Then you can say that $P(x,y) \rightarrow \forall u\;\forall v \;P (u, v)$ is equivalent to $\forall u\;\forall v \;\left( P(x,y) \rightarrow P (u, v) \right)$, so the expression above is equivalent to $$\exists x\;\exists y\; \forall u\;\forall v \;\left( P(x,y) \rightarrow P (u, v) \right).$$

  • 0
    Thanks for the formula clarification. I'm sure I'll use this in my attempts to prove it :)2011-10-25