# 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

## 1 Answer

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
• Congrats on 50k ^_^ Jul 2 at 19:09