How to create tableaus for predicate logic

Question

i know how to create them for propositional logic and i know the rules for quantifiers but i'm confused about how to deal with predicates and functions. r there any rules for them as well?

for example, im stuck on this at the moment:

$$\exists xR(x)\wedge \forall x(R(x)\rightarrow R(f(x)))$$

thanks

Answer 1

There are no rules for them because we do not need them...

When we "instantiate" $\forall$ with e.g. $a$ [i.e., for signed tableau, we apply the rule : $(T\forall)$ ] in the formula : $\forall x (R(x) \to R(f(x)))$ what we get is :

$R(a) \to R(f(a))$.

The only thing to take care of, is that now also $f(a)$ is a term to be used for future application of the "instantiation" rule.