Wolfgang Schwartz asks here if there is a “canonical” way to build free-variable tableaux which are guaranteed to close if the original formula is valid. It seems to me that this must be the case, since free-variable tableaux are a complete proof method. But maybe I don’t understand the question.

The point of free-variable tableaux is to postpone substitutions of strong quantifiers until such a substitution results in a closed branch. So instead of expanding a branch containing ∀*x A*(*x*) by *A*(*t*) for all possible *t*, you keep the free *x* around until you get a formula ¬ *B* on the branch where *A*(*x*) and *B* unify. Closure, i.e., the actual substitution of *x* by a term only happens when this is the case. So at each stage, you should *check* if you can apply Closure (i.e., if you can close the branch) but you don’t actually apply it until you can.

Hi, that’s what I meant by the “greedy Closure strategy”. But it doesn’t always work. Consider a tableau with rootAx(Ey(Fy & ~Fy) & Gx & ~Ga v Ey~Gy & Gx)This can be closed if and only if x is unified with the new constant chosen for y. But greedy Closure will always unify x with a, creating an infinite tableau.The completeness of FVT only means that for every valid formula there exists a closed tableau. There needn’t be a mechanical procedure for tableau expansion that always results in a closed tableau. (To my knowledge there is also no such procedure for axiomatic calculi, which is why the common completeness proofs are all non-constructive.)

Oh, I see what you mean now. The unification has to happen globally, not on each branch separately. To do this efficiently is tricky, as you have figured out. There are ways to do it without backtracking, see e.g., this paper by Martin Giese: Martin Giese. Incremental Closure of Free Variable Tableaux. [gzip’ed PS] Intl. Joint Conf. on Automated Reasoning, IJCAR 2001 Siena, Italy, 2001.For any complete proof procedure, there is a “mechanical procedure” which will result in a proof for any valid formula: try all proofs. But what you want is a “straight-forward” procedure that will start with the formula and incrementally construct a proof (without, as it were, throwing anything away). For axiomatic calculi, you could do this: Pick some complete search procedure for sequent calculus (ordinary tableaux would work too). Define a mapping from sequents to formulas in the usual way:φ(A1, … An ⇒ B1, … Bm) = (A1 ∧ … ∧ An) → (B1 ∨ … ∨ Bm)If S is the sequent you want to prove, start with φ(S). If your sequent search procedure generates an upper sequent S’, add the axiomatic derivation of φ(S) from φ(S’) to the top of your proof, until you are left with axioms A → A.

Thanks! I’ll have a look at the Giese paper as soon as my computer is working again. I was also thinking about the sequent detour to axiomatic proofs after posting my comment. If I recall correctly, David Bostock actually gives a completeness proof for axiomatic systems along these lines in his book ‘Intermediate Logic’. I guess I’ve really been confused about the availability or not of ‘canonical’ proof procedures. After all, in most deductive systems you can combine many small deductions into one big deduction. So another mechanical, non-backtracking procedure for axiomatic systems would be to arrange all possible deductions below each other in one huge deduction. But that’s obviously a useless algorithm. As you say, what really matters is that the procedure is somehow non-redundant and straight-forward.