Truth Trees in QL: Example 1

We will test the following argument for validity:

(x)Fx & (x)Gx
(x)(Gx Hx)
(x)Hx

We begin our tree with the premises and the negation of the conclusion. The reason why? It's the same as in PL. Every truth-tree is a test for consistency. If the premises and the negation of the conclusion are inconsistent, then the argument is valid.

1.     (x)Fx & (x)Gx   checked conjunction. Used rule for conjunctions.
2.     (x)(Gx Hx)      
3.     ~(x)Hx   checked negation of quantified statement. Used quantifier negation.
4.     (x)~Hx      
5.     (x)Fx     left oonjunct of 1.
6.     (x)Gx   checked Right conjunct of 1
7.     Ga     Instantiated 6.
8.     Fa     Instantiated 5.
9.     ~Ha     Instantiated 4
10.     Ga Ha   checked conditional - use branching rule for conditionals
    /   \    
11.   ~Ga   Ha    
    X   X