Finite methods in 1-order formalism
by
Lew Gordeew
Tuebingen University, Germany

FINITE METHODS IN 1-ORDER FORMALISMS

L. Gordeev

Extended Abstract.

Familiar proof theoretical and especially automated deduction methods sometimes accept infinity where in fact it can be omitted. One example deals with the infinite supply of variables admitted in deductions, another - with infinite-branching rules. We consider classical formalisms only, to which constructive formalisms can be reduced, if necessary, by Shanin-style interpretations. In the former case, for any natural number m>2, call m-variable logic a chosen Hilbert-Bernays', Tarski's or Henkin's formalism of predicate logic (with or without equality) whose variables (whether free or bound) are restricted to the initial segment VARm = vo, ..., vm-1, which is based on the rule of inference modus ponens. Unlike the familiar unrestricted case, Gentzen-style cutfree sequent calculi are not suitable for m-variable logic, as they require infinitely many distinct eigenvariables. In fact, cutfree sequent calculi over VARm turn out to be decidable; on the other hand, 3-variable logic is undecidable, while the whole 1-order logic is already interpretable in 4-variable logic. Therefore, we replace sequent calculi by the appropriate Herbrand-style formula rewriting systems, called nested sequent calculi, which simulate rules of inference on arbitrary subformula levels. The main difference is as follows. Gentzen-style reductions, i.e., rules of inference under the interpretation "the conclusion reduces to the premise(s)", require several "dismantling" steps in order to make a chosen subformula the principal formula of of the corresponding expanded sequent, before it can be properly reduced; these auxiliary steps usually require new eigenvariables. But in order to economize derivability, one would often prefer to reduce that subformula immediately, i.e., to replace it with the reduced subformula without changing the environment. The later idea leads to our (cutfree) formula rewriting systems, in VARm, which we also call m-variable nested sequent calculi. As compared to Gentzen's reductions, our reductions include the following crucial rules:

1.A[x/y] -> / 2./ -> D, if x is not free in D 3./ D -> /(A D), if x is not free in D 4. xA -> A[x/y]

Combining these rules enables us to avoid eigenvariables. For example, the following reduction chain (B any formula, L literal) reducing A = /(B(x) xL(x)) ¬L(x) to the truth T serves as a proof of A, where ->i stands for the rewrite rule i.

A ->1 /(/(x) xL(x)) ¬L(x) ->2 /(x) xL(x)) ¬L(x) ->4 /(x) L(x) ¬L(x) -> T

Note that Gentzen-style derivations of A require new variables, in order to separate x occurring in / from x occurring in L(x). Generally, cut elimination theorem holds for m-variable nested sequent calculi, although it fails for Gentzen-style m-variable sequent calculi for m>2. Having this we obtain

Theorem 1.

Hilbert-Bernays' m-variable logic and m-variable sequent calculi both have the same derivable formulae.

Since Tarski's and Henkin's m-variable logics are both interpretable in Hilbert-Bernays' (m+2)-variable logic (with equality), the theorem also provides us with cutfree proof systems which approximate these m-variable formalisms. On the other hand, it turns out that every valid 1-order formula A whose variables are restricted to VARm is provable in the (m+2)-variable logic extended by a suitable axiom expressing that two binary predicates not occurring in A are Tarski's conjugated quasi-projections. In fact, this axiom is inessential in the spirit of Tarski's programm of finite-variable formalization of set theory. For let S be a given finitely axiomatizable 1-order set theory like Goedel-Bernays' system or Quine's New Foundation (say) which admits those quasi-projections. By standard arguments, we can just as well assume that S is a fixed 1-order sentence with n distinct variables. Now let A be an arbitrary 1-order formula in VARm, as above. We ask if A is valid in S, i.e., deducible from S in 1-order logic. By the above, we arrive at the following

Theorem 2.

A is valid in S iff an implication S -> A is derivable in Hilbert-Bernays' 2+max(m, n)-variable logic specified to the language of S + A.

By Theorem 1, this enables us to reduce the validity in S to the derivability in the corresponding finite variable nested sequent calculi. From the viewpoint of automated deduction, the difference is as follows. Usual theorem provers correlate the depth of proof search either with the number of eigenvariables admitted (in Gentzen-style cutfree systems) or with the number of copies of clauses used (in resolution-type systems). Therefore, new proof search formulae can grow very fast as they usually require substitutions of new variables or terms proper for all occurrences of (some) old variables. Since the weight of these new variables is parametrical in proof search depth, the resulting "global" substitutions will multiply the weight of the average proof search formula. In contrast, substitutions restricted to a fixed finite variable domain don't lead to any overweight. We estimate that rewritings in the nested sequent calculi at most double the weight of formulae, - this can accelerate proof search, accordingly. Our second example deals with automated deduction in Peano Arithmetic (PA). It is well-known that standard rules of induction are insufficient for the sake of cut elimination in Gentzen-style sequent calculi. On the other hand, replacing finite rules for quantifiers by infinite-branching omega rules in order to make induction rules obsolete will obviously prevent natural proof search. So we try to eliminate cuts in the presence of finite-branching induction rules. By Gödel's "Dialectica" interpretation, we can reduce the problem to the corresponding quantifier-free cut elimination, which in fact can be simulated in standard sequent calculi for Primitive Recursive Arithmetic (PRA). For the sake of brevity, first consider "preliminary" case where predecessors of cut formulae aren't affected by the rules for primitive recursion. In this case, we argue by induction on the complexity of cut formulae C. If C is a literal, the elimination is easy. Otherwise, C = A / B or C = A B. In order to reduce these cuts, by inductive hypothesis, it will suffice to to prove the inversion lemma using cuts of smaller complexity - namely, cuts on A and/or B. While constructing these inverse derivations, only principal formulas of the rules of induction require special treatments. That is, if C is the inductive formula, we have to pass from the inverse premises to the inverse conclusions in which C turns into A, B. This can be expressed by the new (still finite-branching) rule of inductions. For example, if C = A / B, the new rule in question has the conclusion (a one-side sequent) ß, A(s), B(t) and four premises: ß, A(0), ß, B(0), ß, ¬A(x), ¬B(x), A(x+1), ß, ¬A(x), ¬B(x), B(x+1). Notably, principal formulas of our new induction rules have smaller complexity than principal formulae C of the original rules of induction. We generate these new rules by recursion on the complexity of their principal formulae from the standard induction rule with the conclusion ß, F(s) and two premises ß, F(0) and ß, ¬F(x), F(x+1). The new rules have all "nice" properties of the standard rule which were used in previous cut reduction arguments, which completes the proof in the "preliminary" case. In the general PRA-case, we have to eliminate cuts on atomic equations, or their negations, between primitive recursive terms. This elimination runs by simultaneous induction on the depth of the corresponding primitive recursion rule and the functional complexity of the terms. In the main subcase, we apply the same inversion techniques as in the "preliminary" case. That is to say, we view canonical primitive recursive definitions of f(s, t)=a as propositional definitions by cases with respect to the conditions s=0 and s>0 having smaller functional complexity. This yields the following

Theorem 3.

There is a constructive sequence of valid finite-branching rules of induction such that the resulting extended Gentzen-style cutfree sequent calculus in the language of PRA captures the derivability in PRA.

Conjecture.

It is very likely that an analogous constructive sequent calculus extension of Gödel's "Dialectica" formalism T would approximate the derivability in PA.

Date received: March 2, 1999