I was wondering how to distinguish between developing predicate logic with (∀x) and (∃x) to forms such as Fa or Fb. What rules tells us an argument or conclusion should be developed with an a or b objet ?
For example, here is the development of a tree where Gb is used instead of Ga
Thank you for your help
When you eliminate/instantiate a $\exists$ (or a $\neg \forall$, which is effectively a $\exists$ claim as well) you need to make sure that the constant that you are substituting for the quantified variable is one that does not already occur in that branch of the tree. Thus, for example, if you already used an $a$ earlier in the branch, then you cannot use $a$ again. So note, for example, that on line 10, when they apply the $\exists$ rule on line 9 of the right branch, they introduce a second constant $b$, since you are already using a constant $a$.
Also, you only instantiate a $\exists$ claim just once. This is because once you get $P(a)$ from $\exists x \ P(x)$, then satisfying $P(a)$ will also satisfy $\exists x \ P(x)$, so no need to work with the $\exists$ statement again.
The $\forall$ (or $\neg \exists$) rule, on the other hand, has no restrictions as to what constant can be used to substitute for the quantified variable. In fact, for every constant that exists in the branch, you should instantiate the $\forall$ claim with that, since a claim like $\forall x \ P(x)$ claim will only be satisfied if you have $P(a)$, $P(b)$, etc. So as long as the branch is still open, you need to instantiate a $\forall$ claim with every constant you have introduced. You can nicely see this happening on lines 12 and 13. Note that on line 10 that applies a $\neg \exists$ rule to line 9 in the left branch, you only instantiate it with an $a$, since that was the only constant present at the time, but had that branch not closed, and had you introduced a $b$ in that branch later, then you should have instantiated that same $\neg \exists$ with that $b$ as well.