By decidability (or computability) we mean whether we could mechanically establish that a specific wff is a tautology.

When we are working with predicate logic there will be no problem as long as we are working with monadic or one-place predicates.  The difficulty begins with dyadic predicates and the use of quantifiers.

Here is an example of an argument form for which we can show the derivation very easily:

AxEy(Fxy->Gxy) |- ExAy(Fyx->Gyx)

1.  AxEy(Fxy->Gxy)     Ass
2.  Ey(Fay->Gay)          1  UQ elim
3.  Fab -> Gab               2  EQ elim (x=b)
4.  Ay(Fyb->Gyb)          3  UQ int
5.  ExAy(Fyx->Gyx)      4  EQ int
        remember we must instantiate beginning with the outermost quantifier, but we may generalize in any order we choose

Now let's try a consistency tree.

Do you  see the problem?  Because of our need to adhere to the new name rule we cannot close the branches.
And we cannot make some exception to the new name rule without the risk that in any given case we may in fact not have a valid pattern.  There is really no way around it, and for this reason we have to say that predicate logic is not decidable.

This realization dashes the hopes for symbolic logic as a technique for deciding which mathematical formulas could be proven true, the original goal of pioneers in the field.  Something like Fermat's Last Theorem could not be shown to be either provable or not provable in advance.  If someone advances an acceptable proof, then we know that obviously it is provable, but the fact that no proof might be presented does not itself rule out the possibility.

Thought question:  What are the wff's to which this applies?   Why?