branching

In this file, we give an example of a tableau proof of the following branching formula: exists x, P x -> P a /\ P b, both in outer and inner Skolemization. We start by defining the drinker formula using the extended syntax:

In the proofs (be it in outer or in inner), we create two metavariables by instantiating the formula twice, and replace one of them by a and the other one by b. Here, we do not create any new skolem symbol.

We start by creating a new free variable X.

Then, the proof progresses as expected.

Now, we have a branching rule with the negation of the conjunction. Therefore, we have to apply mkBinaryNode instead, and we will have two goals left.

The first branch is the one where the formula on the left is, i.e., here, it will be Neg P(a).

Here, we can directly closed the branch, instantiating X} by [a].

The second branch is the one where the formula on the right is, i.e., here, it will be Neg P(b).

In this case, we need to create a new free variable X2.

Then, we continue by applying the same previous step, where we replace X by X2.

Finally, we claim that this is enough to close the tableau.

Let's see if this is indeed a proof.

Yay!!