Is there an effective decision procedure for determining whether a truth-tree of first-order logic is infinite?

Question

Reading Tomassi's Logic, he says that the truth-tree method is effective in establishing the validity of a valid sequent of first-order logic, and the invalidity of some invalid sequents. However, trees for some invalid sequents will just go on to infinity, and so "we may never be able to establish mechanically that an invalid sequent... is actually invalid" (p. 362). This led me to wonder whether there is an effective decision procedure for determining whether a tree is infinite. Having seen a few infinite trees, they seem like something that a computer should be able to detect (although I don't know much about computing so I haven't much faith in my intuitions here!). And if there were such a procedure, wouldn't first-order logic then be effectively decidable, since given any sequent, we could see whether the tree it produces is infinite or finite, and if it's infinite, then the sequent is invalid, and if it's finite, we can use the tree to see if the sequent is valid or invalid.

Answer 1

Two points.

1. Start off a tree with the premises and negated conclusion of the argument you are interested in. There is indeed a systematic procedure which will either generate a closed tree (showing the argument is valid) or generate a tree with an open branch from which you can read off a valuation which makes everything on the branch true and hence shows the argument you are interested is invalid. But there is no general method of deciding whether this systematic procedure will indeed produce an open branch. As @spaceisdarkgreen says. (And it is provable that there can be no such procedure.)
2. But if you are interested in tableaux methods, Tomassi’s book won’t take you very far (it’s far from a top recommendation). For better options, and alternatives to tableaux systems, see Beginning Mathematical Logic Chap 3, downloadable from https://logicmatters.net/tyl