drinker

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

As this is a bit verbose, some notations (that have to be imported) can be used instead:

These two really define the same formula:

The extended notation, defined in the module ExtendedSyntaxNotation, uses a "quoting" system, i.e., it uses quotes for connectors, variables & arguments of functions and predicates. The correspondance is as follows:

• '! for EAll and '? for EEx, that must be followed by a variable and the token :(, which should then contain a formula F followed by the closing of a parenthesis,
• '||, '&&, '=> and '<=> for, respectively, EOr, EAnd, EImp and EEqu,
• '~ for ENeg,
• P ''(t1 ,, .. ,, tn) for a predicate,
• f '(t1 ,, .. ,, tn) for a function,
• and 'x for a simple variable.

In the outer Skolemization proof, we have to instantiate the drinker formula twice by X then X2 as the first Skolemization step yields f X. We can then instantiate X2 by f X to bring the proof to closure. In TableauxRocq, we can give this substitution as a finite list and automatically translate it to the system's internal substitution type using translate_substitution.

We can now define the proof tree of this formula. This is done by defining the object called ExtendedRuleTree. This object records the extension rule applied, as well as the formula on which it is applied and, potentially, the term it generates.

The first step will be to apply the GammaNegEx rule on the drinker formula, generating the free variable X. This is a unary rule, so in order to build an ExtendedRuleTree, we can make use of mkUnaryNode. Note the use of the double brackets, that are needed to translate the formula from the extended syntax to the internal one.

The second step is to apply the negated implication on the underlying formula.

We can now apply the first Skolemization rule, generating the Skolem symbol f X.

Then, we have to apply back the drinker formula, which generates a new metavariable X2

And replay the same first step.

Now, we claim that there is a contradiction with the substitution X2 -> f X between P X2 and Neg (P (f X)). We can give these two formulas in any order to the utility function mkClosure.

For trivial closures, e.g., with Bot or Neg Top, use mkTrivialClosure which is a constant ExtendedRuleTree, i.e.: exact mkTrivialClosure. Very importantly, this proof must be Defined.

Now, behold the full power of reflection:

In inner Skolemization, we only have to Skolemize once as "X" does not appear in the body of the Skolemized formula. As before, we provide the substitution using a finite list, and call the translate_substitution function.

Let's do the proof.

The proof proceeds as before for the first two steps

We can now apply the first Skolemization rule, generating the Skolem symbol c.

This is enough to have a contradiction.