I have been taught that a formula in a First-Order Tableau is satisfiable if:
- it terminates with at least an open branch
- it has a branch that never terminates
Now, in case I draw a tableau for a formula and this formula doesn't terminate, given that Tableau for First-Order Logic can be proven sound and complete, can I therefore say that:
since the formula I just expands will never terminate therefore it must be satisfiable?
Well, yes.
This is because "it has a non-terminating branch" is one of the defining clauses of satisfiability.