3

Say that the variables $x,y$ of a predicate $P$ are taken from some non-empty set. It is clear that the following statement is true. How should a formal proof look?

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

Lord_Farin
  • 17,743
Daugmented
  • 546
  • 1
    Formal proofs depend on inference rules. – Git Gud Nov 16 '13 at 18:47
  • 1
    It is not a tautology because $\implies$ is a meta-statement. It is the statement that whenever we have a model satisfying the sentence on the LHS, then it does of the RHS. Tautologies are propositions written in the language (usually referring to propositional calculus, and not predicate calculus too, by the way). – Asaf Karagila Nov 16 '13 at 18:54
  • @Asaf What extra knowledge do you have, to decide that $\implies$ is the "meta" implication, rather than the internal implication (which many denote with $\to$)? – Lord_Farin Nov 16 '13 at 18:55
  • @Lord_Farin: No particular knowledge indeed. More of a custom, tradition, convention, and the fact that I personally solved this question at least three times [as a teacher] over the past four years. But you are right, it could be material implication as well. – Asaf Karagila Nov 16 '13 at 18:57

1 Answers1

7

To formally prove a logical implication you need to show that whenever $M$ is a structure for the language including the relevant symbols, if $M\models\exists x\forall yP(x,y)$, then $M\models\forall y\exists xP(x,y)$.

In order to prove that, one has to begin with taking such $M$ then deconstruct the definition of the assumption, $M\models\exists x\forall yP(x,y)$, and reconstruct that $M\models\forall y\exists xP(x,y)$ is true.

If by $\implies$ you actually meant $\rightarrow$, the connective whose truth table is $p\rightarrow q$ is false if and only if $p$ is true and $q$ is false; then the proof should begin with a structure $M$ for the language, and you need to show that $M$ satisfies this statement.

The proof is in fact quite similar to the above one, in this aspect.

Asaf Karagila
  • 393,674
  • Yes, it can be proved using inference rules, but without specifying the inference rules I cannot help you. – Asaf Karagila Nov 16 '13 at 19:24
  • No, if a statement is true, then it cannot be false in any structure. To your second question, you can do this syntactically using inference rules and without using structure; or you can show that in every structure the statement is true. – Asaf Karagila Nov 16 '13 at 19:52
  • I've tried to "expand" it and make purely syntactic proof.. and I keep failing. I see no trick to get from the $\exists x \forall y$ to $\forall y \exists x$. Can you give me a hint? – Zazaeil Jun 23 '21 at 20:04
  • @Sereja: Syntactic proofs depend very much on your exact inference rules, of which there are many. In principle, this should be just basic rewriting. EI on $\exists x$, then $\forall yP(x,y)$, UI on $\forall y$ to get $P(x,y)$; now apply EG to have $\exists xP(x,y)$ and then UG to get $\forall y\exists xP(x,y)$. – Asaf Karagila Jun 23 '21 at 20:09