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

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.

• Yes, it would make it decidable. But order logic isn’t decidable, so there is no such procedure. Jul 2 at 18:11
• I think it may help to consider an example where the infinite-ness of the relevant tree is non-obvious. Let $s(\overline{x})=t(\overline{x})$ be your favorite Diophantine equation; reinterpreting that equation as a formula $\varphi(\overline{x})$ in the language $\{0,1,+,\cdot\}$ of rings, we have that that Diophantine equation has a solution in $\mathbb{N}$ if and only if $\exists \overline{x}(\varphi(\overline{x}))$ is a consequence of the semiring axioms (the "only if" direction isn't quite obvious, but note that every semiring admits a homomorphism from $\mathbb{Z}$). (cont'd) Jul 2 at 22:45
• Let $\rho$ be the conjunction of the finitely many semiring axioms, and consider the status of $$(\star)\equiv\rho\rightarrow\exists\overline{x}(\varphi(\overline{x}))$$ in case the original equation $s(\overline{x})=t(\overline{x})$ has no solutions over $\mathbb{N}$ but non-obviously so. The resulting tree will be infinite but not obviously infinite (think by analogy with the "look for a solution" process, which of course never terminates ...). Jul 2 at 22:47