Wolfgang Schwarz

Identity (equality) in automated semantic tableaux

It's been quiet here. I haven't had much time or energy for philosophy since the pandemic turned me into a stay-at-home dad on top of the regular job(s). At least teaching has finally come to an end a few weeks ago. I've used my newly found free time to build support for identity into the tree prover.

This is something I've wanted to do for a long time. Every five years or so I look into it, but give up because it's too hard. Here I'll explain the challenges, and the approach I chose.

Tree prover update

I've spent some time this summer upgrading my tree prover. The new version is here. What's new:

• support for some (normal) modal logics
• better detection of invalid formulas
• faster proof search
• nicer user interface and nicer trees
• cleaner source

I hope there aren't too many new bugs. Let me know if you find one!

Tableaux Trouble

I have a problem with the new, free-variables powered version of my tree prover (only existing here on my hard disk at the moment): It doesn't terminate on some valid formulas, at least not within reasonable time.

A very nice feature of ordinary tableaux is that there is a mechanical procedure for building a ("canonical") tableau that will always close as long as there is any closed tableau for the input formula. To my knowledge, no such procedure has been found for free-variable tableaux. The problem, I think, is to decide at each stage whether to apply an ordinary expansion rule or the Closure rule. For many trees, it is best to apply Closure after every expansion. But for some formulas, this procedure will leave the tree forever open. The common response to this problem is apparently to try out all possible decisions at every point, using backtracking and iterated deepening of the search space.

Translating Free-Variable Tableaux

A free-variable tableau with root

x(Fx & y~Fy)

closes after 4 nodes and 1 application of Closure. A standard tableau, on the other hand, will have at least 6 nodes because the root formula must be used twice. So translating free-variable tableaux into standard tableaux is not as easy as I once thought. I wonder if it would suffice to add a rule to the free-variable construction that forbids Closure to unify a variable with a constant that first appears after the variable on the branch.

Detecting Satisfiability with Free-Variable Tableaux

Recently I suggested the following restriction on free-variable tableaux:

The gamma rule must not be applied if the result of its previous application has not yet been replaced by the closure rule.

I think I've now found a proof that the restriction preserves completeness:

Let (GAMMA) be a gamma-node that has been expanded with a variable y even though the free variable x introduced by the previous expansion is still on the tree. I'll show that before the elimination of x, every branch that can be closed by some unifier U can also be closed by a unifier U' that does not contain y in any way (that is, y is neither in the domain nor in the range of the unification, nor does it occur as an argument of anything in the range of the unification.) Hence the expansion with y is completely useless before the elimination of x.

Before the y-expansion, no branch at any stage contains y. After the y-expansion, every open subbranch of (GAMMA) contains the formula created by the y-expansion, let's call it F(y). Among these branches select the one that first gets closed by some unifier U containing y in any way. Now I'll show that, whenever at some stage a formula G(y) containing y occurs on this branch, we can extend the branch by adding the same formula with every occurrence of y replaced by x.

At the stage immediately after the y-expansion, the only formula containing y is F(y). And because (GAMMA) has previously also been expanded with x, and x has not yet been eliminated, the branch also contains F(x). Next, assume that G(y) occurs at some later stage of the branch. Then it has been introduced either by application of an ordinary alpha-delta rule or by the closure rule. If it has been introduced by application of an alpha-delta rule then we can just as well derive G(x) from the corresponding ancestor with x instead of y (which exists by induction hypothesis). Now for the closure rule. Assume first this application of closure does not close the branch (but rather some other branch). Then by assumption, the applied unifier does not contain y in any way, Moreover, it does not replace x by anything else. So in particular, it will not introduce any new occurrences of y in any formula, and it will not replace any occurrences of x and y. Hence if G(y) is the result of applying this unifier to some formula G'(y), then G(x) is the result of applying the unifier to the corresponding formula G'(x).

Assume finally that the branch is now closed by application of some unifier U that contains y in any way. Let C1, -C2 be the unified complementory pair. (At least one of C1, C2 contains y, otherwise U wouldn't be minimal.) Then as we've just shown, the branch also contains the pair C1(y/x), -C2(y/x). Let U' be like U except that every occurrence of y (in its domain or range or in an argument of anything in its range) is replaced by x. Clearly, if U unifies C1 and C2, then U' unifies C1(y/x), C2(y/x).

In the other posting I also mentioned that this restriction can't detect the satisfiability of x((Fx y Fy) Gx), which the Herbrand restriction on standard tableaux can. (A simpler example is x((Fx Fa) Ga).) These cases can be dealt with by simply incorporating the Herbrand restriction into the Free Variable system:

Restrict the Gamma Rule?

The following restriction might be a way out of the problems I mentioned in my last posting:

The gamma rule must not be applied if the result of its previous application has not yet been replaced by the Closure rule.

(The gamma rule deals with and formulae; the Closure rule is the rule that allows to replace dummy constants by real constants iff that leads to the closure of at least one branch.)

Counter-Models and Free-Variable Tableau Systems

I'm half-way into programming a more efficient tree prover, based on free-variable tableaux. But now I'm not sure any more if this is really what I want.

The basic idea in free-variable tableaux is that you use dummy constants to instantiate universally quantified formulas, and only replace these dummy constants by real constants if this allows you to close a branch. In automatised tableaux, this dramatically decreases the steps required for certain proofs. For example, my old tree prover internally creates an 860-node tree to prove xy(Fxy zFzz) x y Fxy x Fxx, whereas a free-variable system only needs 12 nodes.

Better trees, big trees

Sometime before christmas, Greg Restall spotted a bug in my tree prover and noticed that it didn't work with Internet Explorer on MacOS X. These problems should now be fixed. I've also started working on an implementation of proofs with identity and function symbols, but I'm not sure if I'll ever finish it.

I actually wrote the tree prover to check the results of another script, which is what I vaguely talk about in the Feedback section. This is what that other script would calculate if I'd ever get it done:

Tree Proof Generator Update

I've spent some more time on the Tree Proof Generator. The algorithm is now a lot faster, more information is displayed during calculation, and there are new buttons to control the drawing.

This formula (the last one on the Examples page) is quite interesting: After the quantifiers have all been dealt with, there are 36 formulas on the tree that have to be broken down by the truth-functional rules. I let it run for several hours. When finally Mozilla ran out of memory it had developed just 25 of those 36 formulas, building a tree with 179797 nodes!

I've got that formula from David Bostock's very fine book "Intermediate Logic", where he says that "the tedium of writing out a completed tableau" for this formula would be "very considerable" (p.177). Indeed.