# Best method to determine if a first order formula is logically valid?

I know there isnt a "standard method" to determine if a formula is logically valid, but i would like to know if there is something you can always try first of all to determine it.

Not all formulas look obviously valid like $\forall x P(x) \rightarrow \exists x P(x)$. This can be proven with natural deduction, if its required.

For example, i think $(\forall x P(x) \rightarrow \forall x Q(x)) \rightarrow \forall x (P(x) \rightarrow Q(x))$ is valid, and i am trying to prove it by contradiction, asumming there is some intepretation in wich it is false, but i can't figure out how to do it.

• For this particular case, let $P(x)$ be "$x=y$" and $Q(x)$ be "$x \ne y$", and let $\{x,y\}$ be your structure. Jun 29, 2013 at 17:53
• @Wyvern666 Actually, the formula you propose isn't valid. Consider an interpretation in which the domain is $\{1, 2, 3, 4\}$, $P$ is assigned $\{1, 2\}$ and $Q$ is assigned $\{3, 4\}$. In this case, $\forall x P(x)$ is false, and hence $(\forall x P(x) \rightarrow \forall x Q(x))$ is vacuously true. But certainly $\forall x (P(x) \rightarrow Q(x))$ is false: not every $P$ is a $Q$. Hence, the antecedent of the big conditional is true, but the consequent is false, so the whole conditional is false. Jun 29, 2013 at 18:02
• @AlexKocurek what is your interpretation for P and Q here?, i dont understand what you mean with "P is assigned {1,2}" Jun 29, 2013 at 20:44
• @Wyvern666 AlexKocurek means, let the the domain be the set {1,2,3,4}, and let the interpretation of P (which is a unary predicate, so its interpretation is a subset of the domain) be {1,2}. So P(1) and P(2) are true, but P(3) and P(4) are false. Jun 30, 2013 at 3:42

1. First order logic is undecidable, so there is (as you note) no mechanical method for determining first order validity. So what's the next best to a mechanical method for trying to establish (in)validity?

2. The trouble with looking for natural deduction proofs is that the introduction rules allow you to deduce more and more complex wffs, and thus don't stop you spinning off down blind alleys (even when there is a proof to be discovered).

3. Better, then, to use a method without introduction rules, where as you grow a proof the length of wffs at least doesn't grow and ideally decreases. Two options spring to mind. One is downward-branching tableau proofs [as in Richard Jeffrey's lovely Formal Logic: Its Scope and Limits, or my Jeffrey-for-Dummies, officially titled An Introduction to Formal Logic]. The other option is certain sequent systems.

4. The tableau system in particular is very student-friendly, and with a bit of practice, on "nice" examples you'll usually find a closed tableau if there is one to be found, and find an open tableau and be able to read off a valuation which falsifies the wff being tested if the wff is invalid. This is perhaps your best buy!

5. For example, let's use a tableau to test $(\forall x P(x) \rightarrow \forall x Q(x)) \rightarrow \forall x (P(x) \rightarrow Q(x))$. We start by assuming that's false (i.e. its negation is true), which comes to assuming

$$\forall x P(x) \rightarrow \forall x Q(x)$$ $$\neg\forall x (P(x) \rightarrow Q(x))$$

The latter is equivalent to

$$\exists x\neg (P(x) \rightarrow Q(x))$$

So, if that's true there must be an object in the domain which satisfies the condition, which we can dub $a$, so

$$\neg (P(a) \rightarrow Q(a))$$

whence

$$P(a)$$ $$\neg Q(a)$$

Now look at the first line. We have to consider cases. We have either the negated antecedent or the consequent:

$$\neg\forall x(Px)\quad\quad|\quad\quad \forall xQ(x)$$

On the right hand branch we immediately have a contradiction, however, because we can instantiate the universal $\forall xQ(x)$ with $a$ to get $Q(a)$.

So look at the left branch. We can continue that

$$\exists x\neg P(x)\quad\quad\quad\quad\quad\quad$$

$$\neg P(b)\quad\quad\quad\quad\quad\quad$$

where we have to use a new name to dub the witness for the existential. And now we are stymied. So the assumption that the original wff is false doesn't lead to contradiction. So it can't be valid.

In fact, we can read off the open branch of the tableau the interpretation with just two elements in the domain -- call them $a$ and $b$ -- where $P(a)$, $\neg P(b)$, $\neg Q(a)$ and it doesn't matter for $Q(b)$. And that interpretation will falsify the test formula! [For a more careful exploration of this kind of thing, if it is unfamiliar to you, see my book.]

• Yes i am familiar with tableu but only for propositional logic. What is your book?. Jun 29, 2013 at 19:22
• Peter Smith, An Introduction to Formal Logic (CUP) -- logicbook.net Jun 29, 2013 at 19:34
• I got it, is the one that says "forallx" at the beggining?, it doesnt mention tableau proofs. In chapter six it teachs a natural deduction system. MMM, is not the same book, i am wrong. Jun 29, 2013 at 19:42