First Order Logic Validation and Universes of Discourse

First Order Logic Validation

A key feature of Willow is its ability to validate truth trees for First Order Logic (Predicate Logic). In order to do this, Willow needs to be able to properly check the following two "predicate logic" rules (see this slide deck for more info):

1. ∃x ϕ(x) can be instantiated with a constant c (which is new in that branch) as ϕ(c)
2. ∀x ϕ(x) can be instantiated with any constant c as ϕ(c)

We now also need to redefine the way that we define an open branch as "finished" since universals do not need to be decomposed. So we add to the definition of a finished open branch that all universals in that branch must be instantiated for every constant in that branch (since otherwise, a contradiction could arise). Thus, we need a way to track the constants in any branch.

Universe of Discourse

The universe of discourse is the domain (group of constants) that are being considered by a set of First Order Logic statements. This is where the TruthTreeNode#universe variable and its handy TruthTreeNode#calculateUniverse function come in. Remember that this validation requires that each universal be instantiated on every constant in that branch (the universal needs knowledge of every constant declared before and after it) and each existential be instantiated on a new constant in that branch (we will soon discuss an alternative rule and how to handle it). Due to these needy constraints, the universe variable holds every constant that has been referenced in the tree up until and including that node's statement. This means that if a node's statement adds new constants, those constants are in the universe of the node (makes sense, right?). Assuming that everything stays updated (which we will discuss shortly), this means that we can now correctly validate that existentials are instantiated correctly; all we have to do is check whether or not the newly instantiated constant is a "new constant" in the universe (i.e. check whether or not it is in its parent's universe).

Updating the Universe of Discourse

We assumed in the last section that each node would have an updated universe (imagining a static tree). In Willow, however, the trees are not static as users can modify them to write their proofs. Every node has the opportunity to add new constants to the universe (for it and all of the nodes proceeding it), so whenever a node's statement is updated its universe is recalculated and propagated downwards to the rest of the tree below it. This ensures correctness of each node's universe. If the structure of the tree is altered, the highest point of alteration will recalculate its universe and propagate that downwards, which will resolve any outstanding issues.

Universal Instantiation

Okay, so we solved existential instantiation, but what about universals? Universals need to know about constants that are declared after it! If universe only knows about constants declared before the universal, how could it be used to solve this? The answer lies within the fact that we only need to check for these conditions to be met on open branches. Since we have a reference to each of the terminators, we can just iterate over the open terminators and check the universe for each of the terminators. The universe must hold every constant declared up until and including that node, and since the terminators are leaves, they must hold every constant from that branch. Thus, we can iteratively go through each open branch and determine whether or not every constant in that branch's (complete) universe has been instantiated [in that branch]. With that, we have validated universal instantiations.

Alternate Existential Instantiation

One issue with FOL Truth Trees is that you can generate unprovable infinite trees. So in order to allow for contradictions (that would be possible without this rule), we also allow the following:

• ∃x ϕ(x) can be instantiated as ϕ(c) for any constant c already in that branch [as a separate branch]

Note that we still require the original existential rule as well, but this amendment to the validation increases flexibility (and thus ease of proof) for some problems.