Using consistency trees to test for the validity of argument forms with quantifiers

is not that different from what have done to test the validity of other argument forms.  The concept is that whenever we have a universal quantifier it is as though we were talking about a conjunction of predicate statements (logical multiplication):  (x)Fx means Fa & Fb & ... & Fn.  An existential quantifier is as though we had a disjunction of predicate statements (logical addition): (Ex)Fx means Fa v Fb v Fc v ... v Fn.  To test an argument form we need to see whether there could be instances that would allow true premises and false conclusions.  However, since we often have to negate expressions, we have to be very careful about respecting our new name rule.

Here are two situations.  The first is not a valid form, the second is.

(x)(Fx -> Gx), (Ex)(Gx & Hx) |- (Ex)(Fx & Hx)

(x)(Fx -> Gx)
(Ex)(Gx & Hx)
~(Ex)(Fx & Hx)
                                                        (x)(Fx -> ~Hx)   applying quantifier negation
Ga
Ha
/                \
~Fa                   Ga
/     \                    /     \
~Fa  ~Ha         ~Fa   ~Ha
          x                          x
open branches, therefore invalid

(Ex)(Fx & Gx), (x)(Gx -> Hx) |- (Ex)(Fx & Hx)

(Ex)(Fx & Gx)
(x)(Gx -> Hx)
~(Ex)(Fx & Hx)
(x)(Fx -> ~Hx)
Fa
Ga
/                        \
~Ga                  Ha
  x                   /    \
                       ~Fa    ~Ha
                         x         x
no open branches, therefore valid

Do note that there are some situations for which the test does not work.  The following, for instance, is a perfectly valid argument:  (x)(Ey)Fxy |- (Ex)(y)Fyx

    1.  (x))Ey)Fxy       / (Ex)(y)Fyx
    2.  (Ey)Fay           1,  UI
    3.  Fab                 2,  EI
    4.  (y)Fyb              3,  UG
    5.  (Ex)(y)Fyx       4,  EG

With the consistency tree, though, we find a problem because of the need to apply the new name rule:

(x)(Ey)Fxy
~(Ex)(y)Fyx
(x)(Ey)~Fyx
(Ey)Fay
(Ey)~Fya
Fab
~Fca

The consistency tree is an example of a mechanical test for validity.  It will work for any argument form in propositional logic and for any form with quantifiers as long as we do not have the kind of situation (certain situations involving polyadic predicates) described above.  However, the fact that there are exceptions (and this goes for any kind of mechanical test) tells us that our quantifier logic lacks the property of decidability, which means that we would know that a particular highly complex expression is valid if in fact we can provide a derivation, but we might not know in advance whether to try.  Since an original goal of symbolic logic had been to establish a method to determine which relationships in mathematics were necessarily true, the recognition of this proved very disappointing.

Practice exercises


Symbolize and use trees to test for validity.

All logic students work hard.  Some individuals who work hard are successful.  Therefore, some logic students are successful.      (invalid)
Some logic students work hard.  All individuals who work hard are successful.  Therefore, some logic students are successful.      (valid)
No students are lazy.  Anyone lazy will not do well.  Therefore, every student will do well.     (invalid)
No students are lazy.  Anyone not doing well is lazy.  Therefore, every student does well.      (valid)
Every student is doing well.  Anyone lazy does not do well.  Therefore, no students are lazy.      (valid)