I'm a novice and I'm trying to understand semantic tableaux in First-Order Logic.
- existential rule makes sense to me, if ∃x A(x) is true, saying "let c by such x" (where c is new constant symbol) it's very natural to me.
On the other hand, the - universal rule is not that clear to me. If ∀x A(x) is true, then A[t/x] if true for any ground term t.
I understand that a ground term is a term with no variables. However, I have the impression that those ground terms must be built only on the constants introduced by rules and other functional symbols present in the formula. Is this true? Why I'm limited to only these ground terms and not others? (there is a ∀ out there)
Maybe it has something to do with Hearbrand's theorem (A closed formula F in Skolem form is satisfiable if and only if it has a Herbrand model)? It's probably not so, I'm just trying to make sense of rule...
Theoretically you can of course instantiate the variable with any variable-free terms, but in practice it makes sense to stick with terms that only use constants that already exist in its branch. This is because if you ever obtain an open branch every non-literal has either been decomposed, or is a universal that has been instantiated with every constant occurring in that branch, then you have an open and finished branch and a model for the statements in the root of the tree. In other words, introducing neew constants that are not needed creates unnecessary work that can delay the tableaux method from reaching its answer.
In sum: the restriction is for practical reasons, not theoretical.