Eliminating my HOL "Meta-Rules"

HOL systems, as I've mentioned before, are not usually specified just as inference rules on statements. Instead, they are specified indirectly, as inference rules on sequents. A sequent is a set of premises and a conclusion, representing a valid argument in the logic. (This is represented symbolically in the form A, B, C,... |- D where A, B, C,... is the set of premises and D is the conclusion. The |- symbol is called the turnstyle.) So, specifying a system via a sequent calculus is a slightly curious practice: rather than just specifying inference rules directly, we specify a system of reasoning which comes up with valid inference rules. Historically, this move to the meta-level is what led to the field we call "proof theory".

My previous approach was to preserve this multi-level structure, calling the sequents "rules" and the sequent inference rules "meta-rules" (since they are rules for creating rules). However, it would be more efficient to eliminate the extra level if possible.

In general, this may be a complicated process. Some sequent derivation rules have special syntactical restrictions, such as "... X and Y share no free variables ...". Also consider sequent rules like "If A,B |- C, then A |- (B->C)". It isn't obvious that there is a simple way to turn a specification of a system in terms of sequent derivation rules into a direct specification consisting of inference rules on statements.

Typical systems, though, will obey a few nice properties. First, adding more premises to a valid sequent will always result in a valid sequent. Furthermore, many sequent derivation rules just propagate along the premises from the sequents they start with to the sequents they produce. For sequents which do that, the job is easy. Consider an example:

"From A, B, C... |- P and D, E, F... |- Q conclude A, B, C... D, E, F... |- (P&Q)"


In this case, we'd just translate the whole thing to the rule "From P and Q conclude (P&Q)". These sorts can be eliminated from the meta-level immediately, which is good (every little bit helps).

Unfortunately, not all cases are so easy. Many inference rules will almost pass along the premises untouched, but make some little modifications to the list. These modifications will usually be to remove specific premises, occasionally to add premises, and quite rarely to modify the internals of premises. The example above, "If A,B |- C, then A |- (B->C)", is one example of this: one premise is eliminated in the process of drawing the conclusion. Getting rid of meta-rules of this sort requires cleverness.

First-order natural deduction systems handle that particular example in a nice way: at any time during reasoning, we may make a new assumption. This can be anything. We keep the list of assumptions that have been made. Now, say we just concluded something, S. One deduction move we can now make is to remove an assumption from the list (call it A), and stick it on the beginning of S with an arrow: A->S is our new conclusion, which is true in the new context (ie, the old context minus one assumption).

This general idea could be extended to any rules which add or eliminate premises: they are seen as just modifying the list of assumptions.

A practical implementation of this sort of idea for Genifer might be to engage in hypothetical reasoning via conditional queries: we make a query with a list of assumptions attached, to be used in addition to the actual facts. However, some issues may come up with respect to the difference between the classical conditional and the probabilistic conditional. I need to consider this more. (The approach is similar to my "rule-level reasoning", but rather than reasoning about rules using conditional queries, we reason about statements...)

This leaves rules which modify the sequents internally. The primary example of this is variable instantiation, but that's handled by unification! So, in summary, it appears to me that my "meta-level" is not needed in Genifer and can be eliminated with a little patience...

All of the above discussion was done with a translation of HOL Light in mind, but could apply to IG or an IG variant equally well.