A Decision Procedure Revisited: Notes on Direct Logic, Linear Logic

and its Implementation by

Gianluigi Bellin and Jussi Ketonen

Theoretical Computer Science 95 (1992) pp.115-142 Copyright 1992 - Elsevier Science Publishers B.V. All rights reserved

Research Sponsored by Advanced Research Projects Agency

and National Science Foundation

Department of Computer Science Stanford University Stanford, CA 94305

This version of the PROCES was printed on August 19, 1997.

Abstract

This paper studies decidable fragments of predicate calculus. We will focus on the structure of Direct Predicate Calculus as defined in in the light of the recent work of Girard on Linear Logic. Several graph-theoretic results are used to prove correspondences between systems of Natural Deduction, Direct Predicate Logic, and Linear Logic. In addition, the implementation of a decision procedure for Direct Predicate Logic is sketched.

1. Introduction

Much of the recent work in Artificial Intelligence (AI) and its applications uses predicate logic as its foundation. Yet, full predicate logic is known to be undecidable. Given an arbitrary formula, one cannot predict whether the formula is provable, and if so, how fast one can verify it. We are faced with the problem of combinatorial explosion: programs exhibiting supposedly intelligent behavior can get swamped in many unexpected ways. This situation can be somewhat remedied with a better understanding of heuristic approaches and programming tricks in universal proof methods such as resolution. However, we feel strongly that this methodology — derived from the everyday practice of AI programming — must be coupled with a better formal understanding of the use of predicate logic. For example, it is intuitively clear that in most situations the full power of predicate logic is never used: our intention is to mechanize simple-minded reasoning. We are led to study decidable fragments of predicate logic. For example, propositional logic is quite sufficient for simple knowledge representation tasks. Even though all known bounds for procedures for checking propositional tautologies are exponential, they are good enough in practice. However, if we go further and add unary predicates (i.e., study decision procedures for full monadic predicate calculus), we are faced with double exponential bounds . Other fragments defined by restriciting the number of quantifiers that can occur also be proven to be decidable with extremely high bounds . We do not view these types of approaches — syntactic restrictions — as intuitively satisfactory. Our intention is not to restrict the expressiveness of our base language, merely the methods of proof and rules of deduction.

The paper of Ketonen and Weyhrauch defines a fragment of predicate calculus — Direct Predicate Calculus (DPC) — by eliminating the use of the rule of contraction. Intuitively, this means that every formula can be ‘used’ at most once in a proof. Thus, ‘tricky’ proofs such as proof by cases are not covered. For example, the formula

∃y.∀x.A(y)⊃A(x),

while provable, is not provable within DPC. It was shown that DPC admits a relatively simple decision procedure.

The work of Girard can be viewed as a logical extension of this research; by defining multiplicative and linear versions of all propositional connectives and their corresponding proof rules, one can gain a more refined analysis of decidable proof procedures.

Our paper will explore the connections between these two approaches. In particular, we demonstrate correspondences between the basic data structures used in Natural Deduction (proof trees), Linear Logic (proof nets), and Direct Predicate Logic (chains). Finally, we will sketch an implementation approach for the decision procedure for DPC.

1.1. Notation

Our basic language is that of pure first-order predicate logic. We are given a language L_{0} consisting of an infinite list of variable symbols x, y, z, …, a list P_{i} (i = 1, 2, …) of predicate symbols of arity n_{i}≥1, and a list of function symbols f_{i} (i = 1, 2, …) of arity m_{i}≥1. The notion of a term and a formula in the language L_{0} is then defined in the usual manner.

Definition: Any variable is a term. If t_{1}, …, t_{n} is a list of terms and f is an n-ary function symbol, then f(t_{1}, …, t_{n}) is a term. If t_{1}, …, t_{n} is a list of terms and P is an n-ary predicate symbol, then P (t_{1}, …, t_{n}) is an atomic formula. If x is a variable and ϕ, ψ are formulas, then so are

¬ϕ, ϕ⊃ψ, ϕ∧ψ, ϕ∨ψ, ∀x.ϕ, ∃x.ϕ.

One can now go on and formulate a system of predicate logic in the expected fashion. Our interest lies in analyzing the notion of provability in this context. For this reason, we need to often distinguish between a term and its occurrence in a proof. For example, the two occurrences of a formula “A” in “A∧(A⊃C)⊃D” might arise in different ways in a proof. We wish to make this explicit by constructing another language L which will allow us to denote any term of L_{0} in infinitely many different ways. L is constructed by assigning to each symbol s of L_{0} a countable list of distinct symbols O_{s}^{1}, O_{s}^{2}, … of the same arity and type.

In general, we use the letters A, B, C, … to denote formulas of L and Γ, Π, Σ, … for finite sequences of formulas. Comma will be used as a concatenation operator for sequences. The symbol “∅” denotes the empty sequence. For any formula A, we use the notation A(t_{1}, …, t_{n}) for A with all the free occurrences of the variable x_{i} replaced by t_{i} for i = 1, 2, . . ..

Define a partial mapping π from the terms and formulas of L onto the terms and formulas of L_{0} by setting

π(O_{s}^{i}) = s

for all symbols and extending this by a straightforward induction to all objects of L. Clearly, the set of pre-images of any term or a formula of L_{0} under π is infinite. We view π as a fibration of the base language L_{0}.

Two terms t, u of L are called similar (t ≈ u) if π(t) = π(u).

A term t of L is separated if any two similar occurrences of subterms in t are distinct elements of L.

For any t in L there is a separated u similar to it. Using this representation one can uniquely identify a term (or a formula) through its position in the proof of some other term or its appearance in some other term. This fact will make our arguments somewhat easier to formulate.

Define a partial order ≺ on the set of all terms and formulas of L as follows:

t ≺ u ≡_{def} t occurs in u.

Thus A ≺ B if and only if A is a subformula of B if and only if A occurs above B in the tree of formulas.

A positive or negative occurrence of a subformula B in a formula A is defined inductively as follows:

— A is positive;

— let B be C∧D, C∨D, ∀x.C(x) or ∃x.C(x): if B is positive [negative], then C, D, C(t) are positive [negative];

— let B be C⊃D or ¬C: if B is positive [negative] then C is negative [positive] and D is positive [negative].

A quantifier is called essentially universal if it is universal in a positive occurrence or existential in a negative occurrence; otherwise, the quantifier is called essentially existential. This terminology is extended to the variables bound by such quantifiers.

A conjunctive subformula in a set of formulas is either (i) a positive occurrence of a subformula of the form A∧B or (ii) a negative occurrence of A⊃B or (iii) a negative occurrence of A∨B. Similarly, a disjunctive subformula is either a positive occurrence of A∨B or of A⊃B or a negative occurrence of A∧B.

1.2. Sequents

A sequent S is a pair of sequences Γ, Δ of formulas, usually written as Γ ⊢ Δ. Γ is called the antecedent and Δ the succedent. For our purpose it is convenient to use the notation

⊢ ¬Γ, Δ,

or even ⊢ Γ, assuming an implicit partition betwen positive and negative formulas in Γ. We set ¬¬B ≡_{def} B. All of the notions of occurrences for formulas can be extended to sequents by inter-

preting sequents of the form ⊢ ¬A_{1}, ..., ¬A_{n}, B_{1}, ..., B_{m} say as implications of the form: A_{1}∧...∧A_{n}⊃B_{1}∨...∨B_{m}.

We define Axioms and Rules of Inference as follows. Axioms are sequents ⊢ ¬A, B such that A ≈ B. An Inference is a relation between sequent(s) — the premise(s) — and a sequent —

the conclusion —, written as usual

\begin{matrix}S_{1} & S_{1} & & S_{2} \\ S & & S \end{matrix}

according to the rules indicated below.

Structural Rules are Weakening and Exchange; Contraction is excluded:

Contraction ; ⊢ Γ, A, A ; ⊢ Γ, A

Logical Rules are ¬, ∨, ∧, ⊃, ∀, ∃ Left and Right.

In this context it becomes essential to decide whether the rules for disjunction and conjunction are given an additive interpretation, e.g.,

Γ ⊢ Δ, A  Γ ⊢ Δ, B  A, Γ ⊢ Δ  ¬B, Γ ⊢ Δ
Γ ⊢ Δ, A∧B  A∧B, Γ ⊢ Δ  A∧B, Γ ⊢ Δ

or a multiplicative interpretation:

Γ ⊢ Δ, A  Π ⊢ Λ, B  A, B, Γ ⊢ Δ
Γ, Π ⊢ Δ, Λ, A∧B  A∧B, Γ ⊢ Δ

Symmetrically for disjunction.

Left Rules  Right Rules

Weakening ⊢ Γ ⊢ Γ, A

Exchange ⊢ Γ, A, B, Δ ⊢ Γ, B, A, Δ

Conjunction

⊢ ¬A, ¬B, Γ ⊢ Γ, A ⊢ Δ, B
⊢ ¬(A∧B), Γ  ⊢ Γ, Δ, A∧B

Disjunction

⊢ ¬A, Γ ⊢ ¬B, Δ ⊢ Γ, A, B
⊢ ¬(A∨B), Γ, Δ  ⊢ Γ, A∨B

Implication

⊢ Γ, A ⊢ ¬B, Δ ⊢ Γ, ¬A, B, Δ
⊢ ¬(A⊃B)Γ, Δ  ⊢ Γ, A⊃B, Δ

Universal Quantification

⊢ ¬A(t), Γ  ⊢ Γ, A(a)
⊢ ¬∀x.A(x), Γ  ⊢ Γ, ∀x.A(x)

where a does not occur in Γ, Δ.

Existential Quantification

⊢ ¬A(a), Γ  ⊢ Γ, A(t)
⊢ ¬∃y.A(y)Δ  ⊢ Γ, ∃x.A(x)

where a does not occur in Γ, Δ.

In addition, the Cut rule has the form

\begin{aligned}⊢ Γ, A & & ⊢ B, Δ \\ & ⊢ Γ, Δ \end{aligned}

where A ≈ ¬B.

In each rule, the indicated formulas in the premise(s) are the active formulas and the indicated formula in the conclusion the principal formula. All the formulas in the indicated sets are side formulas. The active formulas of Cut are the Cut formulas. The active formula(s) are the immediate ancestors of the principal formula and the relation “... is an ancestor of ...” is the transitive closure of “... is an immediate ancestor of ...”.

Derivations are inductively defined as usual. The definition of a branch β in a derivation is also routine. Definition. A derivation D is separated if for every pair of distinct branches β_{1}, β_{2} and every pair of terms t_{1}, t_{2} with t_{1} ∈ β_{1}, t_{2} ∈ β_{2}, t_{1} ≈ t_{2} implies t_{1} ≠ t_{2}.

We work with separated proofs.

1.3. Relations with the Classical System

The relations between the languages L_{0} and L and between Classical and Direct Sequent Calculus could be further explored by introducing in L the notation A^{(n)}, with the meaning A ∘ A ∘ … ∘ A (n times), where “∘” is “∨” in a positive context and “∧” in a negative context. One can then introduce the following approximation of Contraction

\begin{matrix}⊢ Γ, A^{(n)}, B^{(m)}, Δ \\ ⊢ Γ, A^{(n+m)}, Δ \end{matrix}

where A ≈ B.

Next, one may consider a Generalized Cut rule, or Mix

\begin{matrix}⊢ Γ, A^{(n)} ⊢ B^{(m)}, Δ \\ ⊢ Γ, Δ \end{matrix}

where A ≈ ¬B. The trouble with Mix is that it cannot be reduced to Cut: one completely loses control over the number of iterations. Thus Mix must be forbidden from Direct Logic. On the other hand, the rule

\begin{aligned}⊢ Γ, A & & ⊢ B^{(m)}, Δ \\ & ⊢ Γ^{(m)}, Δ \end{aligned}

with A ≈ ¬B, is definable in terms of Cut, and yields an (exponential) bound on the number of needed duplication. The dynamical analysis of Contraction (i.e., with respect to Cut elimination) in classical logic is a main concern and motivation for a logic as ours. However, the issue will not be pursued further in this paper.

The following is clear:

Approximation Theorem. Let S be any sequent in L_{0}. S is derivable in classical sequent calculus LK iff there is a sequent S^{∗} in L, derivable in Direct sequent calculus such that π(S^{∗}) = S.

1.4. Basic Proof Theory

Cut Elimination Theorem: Every derivation D in Direct Sequent Calculus can be transformed into a Cut free derivation D′.

Let D be a cut free derivation of S in which all axioms involve atomic formulas. Without loss of generality, we may also assume that all principal formulas in applications of a Weakening are atomic.

Corollary (Strong Subformula Property): There exists a bijection between the subformulas of S and the active formulas of inferences of D.

Corollary (Midsequent Theorem): Let S be a sequent containing only prenex formulas, derivable in Direct Sequent Calculus. There exists a Cut free derivation D of S and a sequent S_{0} in D with the following properties:

(i): S_{0} results from S by erasing all quantifiers and replacing the variables by terms; (ii): every inference above S_{0} is propositional and every inference below S_{0} is quan-

tificational.

We may assume that different variables are used in different occurrences of quantifiers. Herbrand’s Theorem has nice properties in Direct Logic. We recall the definition

of Herbrand function. In a sequent S, let Qy.A(y) be an essentially universal subformula which lies in the scope of the essentially existential quantifiers Qx_{1},..., Qx_{n}: then y[x_{1}, …, x_{n}] is the Herbrand term associated with Qy.

The Herbrand form S_{H}(x_{1}, …, x_{n}) of a sequent S is the result of erasing all quantifiers of S and of replacing each essentially universal variable with the corresponding Herbrand function. (Here x_{1}, …, x_{n} are all the essentially existential variables in S).

Corollary (Herbrand Theorem):† Let S be a sequent containing only prenex formulas. Then S is derivable in Direct Predicate Calculus iff there are terms t_{1}, …, t_{n} such that S_{H}(t_{1}, …, t_{n}) is derivable in Direct Propositional Calculus.

† The theorem is not true for non prenex formulas. Counterexample:

(∃y.A(y))∨B⊃(∃x.A(x)∨B).

2. Linear logic and Direct Predicate Calculus

Girard’s Linear Logic provides a comprehensive framework in which the above issues can be discussed. The context is particularly stimulating, since connections are exibited between results of Proof Theory, Category and Domain Theory, Linear Algebra and Banach Algebras .

Developing ideas already present in the literature on Contraction free systems and in Relevance Logic (see ), Girard gives an instructive picture of the structure underlying Classical and Intuitionistic Logic.

The connectives of Linear Logic and their dual are organized in 5 levels:

(1) the self-dual linear negation (.)^{⊥};

(2) multiplicative conjunction ⊗ (times) and the dual disjunction ⊔ (par), with their identities, namely, 1 and ⊥;

(3) additive disjunction ⊕ (plus), and the dual conjunction & (with), with the identities 0 and ⊤, respectively;

(4) the exponentials: ! (of course) and its dual ? (why not)

(5) additive quantifiers ⋀ (every) and the dual ⋁ (some).

Linear negation is defined for non atomic formulas, linear implication is defined as multiplicative.

At the moment (November 1988) we are aware of 5 different semantics for Linear Logic: Girard’s Phase Semantics, Coherent Semantics and the interpretation in C^{∗} Algebras ; Lafont’s interpretation in Linear Algebra and Sambin’s in Formal Spaces . †

Sequent Calculi for Linear Logic are obtained by eliminating both structural rules of Weakening and Contraction.

The Multiplicative Fragment (levels (1) and (2)) has logical rules for ⊗ and ⊔

\begin{aligned}⊢ Γ, A & ⊢ Δ, B & ⊢ A, B, Γ \\ ⊢ Γ, Δ, A ⊗ B & ⊢ A ⊔ B, Γ \end{aligned}

the axiom ⊢ 1 and the rule Weakening, but only with the constant ⊥ as principal formula.

It is true, however, that given S, there exists S^{∗} ≈ S such that some subformulas of S are fibrated in S^{∗} and the theorem holds for S^{∗}. We will not pursue this topic here.

† We will not say anything about semantics. The reader of may want do the following easy Exercise for Chapter 1: Direct logic is sound and complete with respect to Phase Structures with 0 = ⊥. In this Chapter we work within the limits of Proof Theory — with the prospect of applications for automatic formalization of proofs.

The Additives (level 3) satisfy the rules

\begin{aligned}⊢ Γ, A & ⊢ Γ, B & ⊢ A, Γ & ⊢ B, Γ \\ ⊢ Γ, A&B & ⊢ A ⊕ B, Γ & ⊢ A ⊕ B, Γ \end{aligned}

and the axiom ⊢ ⊤, Γ (given that ⊤ and 0 are dual, this means “0 linearly implies everything”).

Finally, for the Exponentials (level 4) there are the rules

\begin{aligned}⊢?Γ, A & ⊢ Γ, A \\ ⊢?Γ,!A & ⊢ Γ,?A \end{aligned}

where ?Γ means that all formulas in Γ begin with ?; in addition, Contraction and Weakening are allowed for formulas beginning with ?. It is easy to see that the rule of Mix is not derivable in this system (see Section 1.3 ).

It is clear that Propositional Direct Logic is exactly the Multiplicative fragment with Weakening for arbitrary formulas.

2.1. Proof Nets

In addition to Sequent Calculus, the Proof Theory of Linear Logic consists of the new and suggestive notion of Proof Net. We will be mainly interested in this notion for the Multiplicative Fragment.

Given a set S of propositional formulas in the multiplicative language, a Proof Net comprises the following set of data:

(1) the set S^{≺} of subformulas of S arranged in the obvious tree stucture. A link is the relation between a formula (the conclusion of the link) and its immediate subformulas (the premises of the link);

(2) a set P of Axiom links, i.e., connections between positive and negative occurrences of the same formula (the conclusions of the axiom link). Here we consider axiom links with atomic formulas only. Each occurrence of atomic formula in S^{≺} is a conclusion of at most one axiom link.

A pair (S^{≺}, P) is a Proof Structure for (Multiplicative) Linear Logic if

— (relevance condition) all atoms of S^{≺} are conclusions of exactly one axiom link. (3) A Proof Structure is a Proof Net if it satisfies a graph theoretic condition.

Thus, a Proof Structure for the Multiplicative Fragment is built using the following links, with the condition that every formula occurrence is a consequence of one link and premise of at most one link.

Girard Multiplicative Links

Axioms A A^{⊥}

Times

(A B) / (A ⊗ B)

Par

(A B) / (A ⊔ B)

The graph theoretic condition (3) is defined in terms of trips over (S^{≺}, P). A trip visits the formulas of a proof structure in two directions, ↑ and ↓, the movements being determined by the nature of the link and by arbitrary choices (switches) as follows:

Axioms

A^{∧}, A^{⊥}_{∨}; A^{⊥}^{∧}, A_{∨}

Conclusions

C_{∨}, C^{∧}

Times

Switch L  A ⊗ B^{∧}, B^{∧};  B_{∨}, A^{∧};  A_{∨}, A ⊗ B_{∨};
Switch R  A ⊗ B^{∧}, A^{∧};  A_{∨}, B^{∧};  B_{∨}, A ⊗ B_{∨};

Par

Switch L  A ⊔ B^{∧}, A^{∧};  B_{∨}, B^{∧};  A_{∨}, A ⊔ B_{∨};
Switch R  A ⊔ B^{∧}, B^{∧};  B_{∨}, A^{∧};  B_{∨}, A ⊔ B_{∨};

A proof structure β with n formula occurrences is a proof net if for every position of the switches the resulting trip does not return to the starting point in the same direction in less than 2n steps.

A main theorem of is

Theorem S is provable in Multiplicative Linear Sequent Calculus if and only if there is a P such that (S^{≺}, P) is a Proof Net. (The “if” direction is called Sequentialization Theorem. For a simplification of the proof, see also , Quantifiers in Linear Logic, II.1., Remark 2, p. 21.)

Proof structures for the multiplicative fragment can be extended to a rule of Weakening by using a box: if β is a proof structure (with boxes) with conclusions A_{1}, ..., A_{n}, then the following is a proof structure with boxes:

β
A_{1}...A_{n}
A_{1} … A_{n} B

The list of formulas at the bottom of the box may be regarded as an extended Axiom for the structure outside it. If σ is any cyclic permutation of n + 1, then C_{i}^{∧}, C_{σ(i)}_{∨} (for C_{i} = A_{1}, ..., A_{n}, B) determines the trip at the outside of the box — independently of the trips inside the box.

A proof structure with boxes is defined to be a proof net if for each box both the structure inside each box and the structure outside are proof nets.

The main theorem can be extended to Proof Nets with Weakening Boxes.

2.2. Multiple Conclusion Natural Deduction

Girard’s notion of Proof Net requires us to reconsider the following question: What are the relevant features of Natural Deduction Systems vs. Sequent Calculi?

The issue is not just one of terminology. Both Natural Deduction and Sequent Calculi

(i) create links between occurrences of formulas — roughly corresponding, in informal reasoning, to the sequence of statements in an argument. In Natural Deduction these links are given by the Rules of Inference. In Sequent Calculus they are the relation between active and principal formulas in an inference.

(ii) establish relations between the occurrences of formulas in (i) and the context — roughly corresponding in informal reasoning to the structure of an argument (what are the presuppositions? what is the conclusion?) and conditions for its correctness. For instance, a sequent is precisely a notational device that keeps track of side formulas. In Natural Deduction such specifications are given, e.g., as Rules of Deduction (see , Chapter I). In both formalisms there are restrictions on eigenvariables, i.e., the free variables that become bound in an (essentially) universal quantification. Typically, these restrictions are relations between the active premise of a quantification and its context.

A Sequent Calculus can be characterized as a formal system where (i) and (ii) are local, i.e., given simultaneously by the rules of inference — this is one of the reasons why Sequent Calculus is an efficient mathematical tool. On the contrary, Natural Deduction is a formal system in which (i) is local and (ii) is global.

According to the above calssification, Proof Nets are clearly to be regarded as a Natural Deduction system. A Multiple Conclusion Natural Deduction (MCND) system is one in which formula occurrences are arranged as a directed acyclic graph, rather than as a tree. Proof Net are a MCND system.

This view may encounter objections:

(a) Natural Deduction is a system for deducibility from assumptions as opposed to derivability from logical axioms, as in Sequent Calculus;

(b) essential feature of Natural Deduction is the presence of Introduction and Elimination rules and a certain logical priority of the Introduction rules.

To (a): The present arrangement of Multiplicative Proof Structures is very convenient and economical and makes assumptions and conclusion interchangeable, at the cost of giving up the functional character of the implication rule. However, another MCND system for the Multiplicative Fragment could be designed that has multiple-premise rules for ⊗-Introduction and ⊔-Introduction, multiple-conclusion rules for ⊗-Elimination and ⊔- Elimination, as well as Introduction and Elimination rules for Linear Implication of more traditional kind. Constraints to guarantee consistency of such system could easily be described by adapting the “No Short Trip” condition.

To (b): Proof Nets are a system with only Introduction rules, thanks to the duality of the connectives. However, something of the intuition behind the Introduction-Elimination classification is preserved, in a certain priority of the connectives themselves: for instance, the notion of ⊗ seems to be more easy to understand than that of ⊔ and ⊕ easier than &.

2.3. Proof search in Sequent Calculi

The above considerations are relevant to the discussion of more mundane issues, like the computational content of derivations in Classical Logic. It is inefficiently represented by the standard systems of Sequent Calculus and Natural Deduction.

Prawitz’s treatment of Intuitionistic Logic in Natural Deduction seems definitive from the point of view of Proof Theory: the proofs of very strong results (e.g., Strong Normalization) are elegant and the weak spots (e.g., the permutability of ∃-elimination and ∨-elimination) may be regarded as relatively minor inconveniences. Also, the computational content of Intuitionistic Logic is well represented by Natural Deduction, given the Curry-Howard analogy with λ-calculus. However, Prawitz’s Natural Deduction system for Classical Logic is inadequate, since it uses essentially the negative translation into Intuitionistic Logic.

Sequent Calculi for Classical Logic effectively express semantical ideas and arguments (see Schutte’s Valuations and Girard’s work on the semantics of Cut-free proofs). Computationally, sequent calculus is less satisfactory. For example, the standard algorithm for searching for proofs — the Wang algorithm — (based on the invertibility of the rules of Sequent Calculus (cfr. )), is relatively inefficient even for propositional calculus.

Here we write the tree from bottom up, breaking alternately the leftmost formula in the antecedent (i.e., at the left of ⊢) and the leftmost formula in the consequent (i.e., at the right of ⊢). In a system with Contraction, we also rewrite the formula under consideration in the upper sequent(s). Then we keep going upwards and break formulas on each branch until the process enters a loop on each branch — or, in the case of a system without Contraction, until there is no formula to break.

The very locality of the rules of sequent calculus forces us to neglect the global ‘leitmotifs’ of proofs. For example, the mechanical application of inverted 2-premise rules not only duplicates the work to be done in every succeeding step but may also be unnecessary. The ‘global picture’, i.e., the natural order of application of inference rules, cannot be deciphered through the application of this kind of formalism. The problems presented by the classical resolution approach are similar: again we are faced with the necessity of a global, conjunctive normal form — a transformation that erases the local connections used in natural proof generation.

Consider, e.g., the treatment of the right conjunction rule in a system without Contraction: an additive interpretation must be taken. Notice that this is incompatible with the notion of “formulas as trees”. A multiplicative interpretation would be attractive because formulas in Γ and Δ would be broken just once. However to implement it intelligently, we need a global consideration of the role of the side formulas in the proof.

In terms of Girard’s trips one can effectively express the main task of any reasonable procedure: to continue the search from a formula occurrence of the form A∧B (multiplicative interpretation) one needs two separate ‘explorations’ of the context, one from A and the other from B, or:

Lemma: Any trip in a proof net containing the link

\begin{matrix}A & B \\ A ⊗ B \end{matrix}

has either the form

A^{∧}, ..., A_{∨}, B^{∧}, ..., B_{∨}, (A ⊗ B)_{∨}, ..., (A ⊗ B)^{∧}, A^{∧}

or

A^{∧}, ..., A_{∨}, (A ⊗ B)_{∨}, ..., (A ⊗ B)^{∧}, B^{∧}, ..., B_{∨}, A^{∧},

where here are no visits to A, B and A ⊗ B other than the indicated ones. (see , Lemma 2.9.1.).

3. A Decision Procedure for Direct Predicate Logic

Let S be a set of closed first order formulas of L in prenex normal form. We shall outline below a procedure (and the appropriate abstract data structures) for deciding whether

⊢ S

in Direct Predicate Calculus.

We can consider the Herbrand form S_{H}(x_{1}, …, x_{n}) of S (as in Section 1.4 ). Our problem reduces to finding a substitution σ = (x_{1}/t_{1}, …, x_{n}/t_{n}) such that

S_{H}(t_{1}, …, t_{n})

is provable in Direct Propositional Logic.

3.1. Paths

The first step of the procedure is the search for an open path through S_{H}(x_{1}, …, x_{n}), i.e., a set P(x_{1}, …, x_{n}) of pairs of atoms (P, P′). Definitions.(i) An open path P is a set of pairs of atomic formulas such that:

(a) if (P, P′), (Q, Q′) are two distinct members of P then P ≠ Q and P′ ≠ Q′. (ii) We say that P satisfies a formula A (in symbols P ↦ A) if there is a pair (P, P′) in P such that either P ≺ A or P′ ≺ A. (iii) Let S be a set of formulas. We say that P is a path for S if

(b) P satisfies some formula in S;

(c) for all conjunctive subformulas AoB in S, if P ↦ AoB then P ↦ A and P ↦ B (relevance condition for conjunctions);

(d) for all (P, P′) ∈ P, P occurs positively in S and P′ occurs negatively in S. (iv) a path P for S is minimal if no proper subset P′ of P is a path for S.

3.2. Chains

Consider the tree S_{H}^{≺} of all subformulas of S_{H}(x_{1}, …, x_{n}), as in Section 2.1 .

It is convenient to mark the conjunctive subformulas of S_{H}^{≺}:

Multiplicative Links

And

¬A  ¬B  A  B
. . . . . . . . . . .
¬(A∧B)  A∧B

Or

¬A  ¬B  A  B
. . . . . . . . .
¬(A∨B)  A∨B

Implies

A  ¬B  ¬A  B
. . . . . . . . .
¬(A⊃B)  A⊃B

Consider the tree S_{H}^{≺}(x_{1}, …, x_{n}), together with an open path P(x_{1}, …, x_{n}) and a substitution σ = (x_{1}/t_{1}, …, x_{n}/t_{n}) such that

(α) If (P, P′) ∈ P, then P [x_{1}/t_{1}, ..., x_{n}/t_{n}] and P′[x_{1}/t_{1}, ..., x_{n}/t_{n}] are similar.

Then the pair (S^{σ,≺}, P^{σ}) with S^{σ,≺} = S_{H}^{≺}(t_{1}, …, t_{n}) and P^{σ} = P(t_{1}, …, t_{n}) (closed path) can be regarded as a proof structure in the sense of Section 2.1 , except that in Direct Logic the relevance condition is relaxed to a relevance condition for conjunctive subformulas. Definitions. (i) For A, B ∈ S^{σ,≺} A ≠ B, say that A and B are connected (write A ∥ B) if there is a pair (P, P′) ∈ P^{σ} such that P ≺ A and P′ ≺ B (or viceversa). (ii) Let X, Y ∈ S^{σ,≺} be such that X ⊀ Y and Y ⊀ X, with A ≺ X and B ≺ Y. We write X_{A} −_{B} Y if A||B. (iii) For X ∈ S^{σ,≺} we write _{A}X_{B} if AoB is a conjunctive subformula of X. (iv) Let C = C_{0}, …, C_{n} be a set of subformulas in (S^{σ,≺}, P^{σ}) with n > 0 and C_{i} ≠ C_{j} for all 0≤i ≠ j≤n. C is called a cycle if

AC_{0}_{B} −_{A_{1}} C_{1}_{B_{1}} − ... −_{A_{n}} C_{n}_{B_{n}} −_{A} C_{0}.

The graph theoretic conditions that select the proof structures corresponding to a correct proof are the following:

(β) If P ↦ A∧B, then not A ∥ B. (γ) There is no conjunctive cycle.

3.3. The Main Theorem

The main theorem (Theorem 4.4.) of is:

Theorem For any sequence t_{1},..., t_{n} of terms, the sequent S_{H}[x_{1}/t_{1}, ..., x_{n}/t_{n}] is provable in Direct Sequent Calculus if and only if we can find a minimal path P for S_{H}[x_{1}/ t_{1}, ..., x_{n}/t_{n}] satisfying:

(α) If (P, P′) ∈ P, then P [x_{1}/t_{1}, ..., x_{n}/t_{n}] and P′[x_{1}/t_{1}, ..., x_{n}/t_{n}] are similar.

(β) If AoB is a conjunctive subformula and P ↦ AoB, then not A ∥ B.

(γ) There is no conjunctive cycle.

3.4. An Example

Consider the set of formulas

S = {A∧B, A∧¬B, ¬A∧¬B, ¬A∧B}.

Construct the tree of subformulas S^{≺}: every path P for S^{≺} creates a conjunctive cycle. For instance:

\begin{aligned}A & B & A & ¬B & ¬A & ¬B & ¬A & B \\ & A∧B & & & A∧¬B & ¬A∧¬B & ¬A∧B \end{aligned}

Therefore S is not provable in Direct Logic. To find a set S′, provable in Direct Logic, such that its projection π(S′) is S, notice that we must break the conjunctive cycle into two loops. The simplest S′ will have the form

S′ = {(A∧B, A∧B), A∧¬B, (¬A, ¬A)∧(¬B, ¬B), ¬A∧B}.

In other words, we need to duplicate both a ‘top level conjunction’ and the subformulas of a conjunction.

¬A  ¬A ¬B  ¬B
A B A  ¬B (¬A, ¬A)  (¬B, ¬B) ¬A  B  A B
A∧B  A∧¬B  (¬A, ¬A)∧(¬B, ¬B)  ¬A∧B  A∧B

4. Some Properties of Graphs

In this section we formulate abstractly some properties of graphs to be applied to formulas in trees of subformulas.

4.1. Definitions

Let G = (V, E) be a graph with V finite and let F be a set of subsets of V. Also, let C be a set of distinguished elements of F, such that each C ∈ C is partitioned by some elements A_{1}, …, A_{n} of F. (The set of singleton subsets of) V will be interpreted as the set of all atomic formulas, F as the set of all formulas and C as the set of conjunctive subformulas, where each C ∈ C is written in conjunctive normal form as A_{1}∧ … ∧A_{n}. Finally, E as the set of connections on V determined by a unification of positive and negative atoms.

(i) For A, B ∈ F with A ∩ B = ∅, say that A and B are connected (write A ∥ B) if there is an edge e in E with vertices v_{1} and v_{2} such that v_{1} ∈ A and v_{2} ∈ B.

(ii) Let X, Y, A, B ∈ C. We write X_{A} −_{B} Y if X ∩ Y = ∅, A ⊂ X, B ⊂ Y and, moreover, A ∥ B. Think of A and B as “doors” of X and Y, respectively.

(iii) We write _{A}X_{B} if A and B are different sets in the partition of X. A chain is a sequence X_{1}, …, X_{n} such that Y −_{A_{1}} X_{1}_{B_{1}} − ... −_{A_{n}} X_{n}_{B_{n}} − Z.

(iv) A chain is pure if for all i ≠ j with 1≤i, j≤n, X_{i} ≠ X_{j}. Let C = X_{1} − ... − X_{n} be a nonempty pure chain.

(v) _{A}Y_{B} − C −_{A} Y is called a cycle.

(vi) Y_{B} − C −_{A} Y is called a loop if A = B. Y is the exit of the loop.

(vii) A chain C is terminal if there is a formula in C from which C cannot be continued. (viii) X ≫^{1} Y iff there is a loop

L : Z_{A} − ... − X − ... −_{A} Z

and either Y = Z or there is a pure chain

C :_{A} Z_{B} − ... − Y.

We summarize this condition by saying that Y is dominated by the loop, which X belongs to.

(ix) X ≫ Y iff X ≫^{1} Y and not Y ≫^{1} X.

Remark. Let L be a loop with exit Z and let C be a pure chain starting with Z. If C ∩ L ≠ {Z} then there must be a cycle.

Indeed, suppose

L : Z_{A} − ... −_{C} U_{D} − ... −_{A} Z

and

C :_{A} Z_{B} − ... −_{E} U − ... − Y.

Now either

EU_{D} − ... −_{A} Z_{B} − ... −_{E} U  or  _{E}U_{C} − ... −_{A} Z_{B} − ... −_{E} U

or both are cycles, depending on whether E = C, E = D or C ≠ E ≠ D, respectively.

4.2. Basic Properties of Chains

Lemma 1. Suppose no chain is a cycle. Then ≫ is a strict partial ordering.

Proof. To show that X ≫ Y and Y ≫ Z implies X ≫ Z, we need only to show that for all U, V, W, U ≫ V and V ≫^{1} W implies U ≫^{1} W. Indeed, assume X ≫ Y and Y ≫ Z. Then certainly X ≫^{1} Z. Moreover, given Y ≫ Z, if Z ≫^{1} X, then Y ≫^{1} X, a contradiction.

Assume there are loops L_{1}, L_{2} and pure chains C_{1}, C_{2}

L_{1} : U_{A} − X_{1} − ... − X − ... − X_{n} −_{A} U
C_{1} : _{A}U_{B} − U_{1} − U_{2} − ... − U_{i} −_{E} Y
L_{2} : V_{C} − X′_{1} − ... −_{F} Y_{G} − ... − X′_{m} −_{C} V
C_{2} : _{C}V_{D} − V_{1} − V_{2} − ... − Z

Clearly, either _{E}Y_{G} or _{E}Y_{F} or both, depending on whether E = F, E = G or F ≠ E ≠ G, say the latter.

Then we claim that

U_{B} − ... −_{E} Y_{G} − ... −_{C} V_{D} − ... − Z

is a pure chain. Since there are no cycles, C_{2} ∩L_{2} = {V }, as remarked above. On the other hand, if U^{∗} ∈ C_{1} ∩ C_{2}, then either we have a cycle

HU_{L}^{∗} − ... − Y − ... − V − ... −_{H} U^{∗}

or

V_{D} − ... −_{H} U_{L}^{∗} − ... − U − ... − X

is a pure chain and Y ≫^{1} X, against the hypothesis.

Let T be a subset of C such that for each X, Y ∈ T if X ≠ Y, then X ∩ Y = ∅ and for each A ∈ C, if X ∩ A ≠ ∅ then A ⊂ X. The intended interpretation of T is the set of top level (i.e., outermost) conjunctive subformulas. Consider the set Chain of chains of elements of T.

Lemma 2. If Chain contains an infinite chain C^{∞} but no cycle, then the relation ≫ is nonempty and there is X_{0} ∈ T such that for no Y ∈ T, X_{0} ≫ Y.

Proof. Since there is no cycle, for some C ⊂ C^{∞} there is a C′ ∈ Chain such that

C′ = L′ − ... − C − ... − L′′

where L′ and L′′ are loops.

Let W be the exit of L′ and X an element of L′ different from W. Suppose L^{∗} is another loop, W ∈ L^{∗} and X is dominated by L^{∗}, then it is immediate to see that X and W belong to a cycle. Hence X ≫ W and ≫ is nonempty.

An X_{0} minimal with respect to ≫ exists by finiteness of V and Lemma 1.

5. Proof of the Main Theorem

This proof details the procedures by which we can compute the proof data structure from the representing chain and vice versa.

5.1. From Proofs to Chains

Consider first an application R_{1} of Weakening in D, let A be the principal formula, and R_{2} the inference immediately below R_{1}.

If A is passive in R_{2}, then we can certainly permute R_{1} and R_{2}. Thus we may assume that for every Weakening R_{1}, the principal formula A of R_{1} is either

(i) active in the inference R_{2} immediately below, or

(ii) that R_{2} is also a Weakening with principal formula B and that the next inference R_{3} is a one-premise rule, say ∨-Right, with B and the descendant of A as active formulas.

If (i) and R_{2} is a two-premises rule, then we can delete the entire branch ending with the other premise of R_{2} and replace R_{1} and R_{2} with a sequence of Weakenings.

In case (ii) we can replace R_{1}, R_{2} and R_{3} by a unique application of Weakening with principal formula A∨B. And so on.

The point of this standard fact is that, by applying Weakening as low as possible we obtain a derivation in which every active formula in a two premise rule has some ancestor in an axiom. We assume that D has this property.

Now we construct the desired path P by induction on the length of the derivation D of S. We let P be the set of (P, P′) such that ⊢ P, ¬P′ (or ⊢ ¬P′, P) is an axiom of D. If D consists of an axiom or if the last rule of D has one premise only, then the proof is trivial.

Suppose it has two premises S_{1} and S_{2}, with subderivations D_{1} and D_{2}, active formulas A, B and principal formula, say A∧B. By induction hypothesis there are paths P_{1} and P_{2} for S_{1} and S_{2}, respectively, satisfying the required conditions. The pairs of formulas in P_{1} and P_{2} correspond to axioms of D_{1} and D_{2}. Construct S^{≺} by adding the appropriate conjunctive link below the subformulas-trees of A and B, etc.

Let P = P_{1} ∪ P_{2}. Since D is separated, P satisfies part (a) in the definition of path (4.2). P obviously satisfies parts (b) and (d). By the argument above P_{1} ↦ A and P_{2} ↦ B, so P satisfies also (c), the relevance condition for conjunctive subformulas. The fact that P is minimal is immediate from the inductive hypothesis. Condition (α) is trivial. The axioms of D_{1} and D_{2} are distinct, so P satisfies condition (β).

To check condition (γ), since a cycle cannot occur only inside S_{1}^{≺} or S_{2}^{≺}, we need to consider only infinite conjunctive chains containing A∧B, say

C :_{F} X_{C} − ... −_{D} A∧B_{E} − ... −_{F} X.

Every chain containing conjunctive subformulas of both S_{1}^{≺} and S_{2}^{≺} must contain A∧B. If

C_{1} : X_{C} − Y_{n} − ... −_{D} A∧B

and

C_{2} : A∧B_{E} − ... − Z_{m} −_{F} X

are both pure, then all Y_{i} ∈ S_{1}^{≺} and all Z_{j} ∈ S_{2}^{≺}. But X cannot belong both to S_{1}^{≺} and to S_{2}^{≺}.

Thus we may assume that X is A∧B, C ≺ A and F ≺ B. If, however, there was a conjunctive subformula, say C∧D ≺ A, then we would have a cycle in S_{1}^{≺}, against the hypothesis. Thus C = D = A, i.e. C_{1} is a loop (and similarly for C_{2}).

5.2. From Chains to Proofs

We have S^{≺} and P satisfying the conditions. The proof is by induction on the number of logical symbols in S, plus the number of atoms in S which do not occur in any (P, P′) ∈ P.

The case of all formulas in S that are not satisfied by P is clearly handled using Weakening.

If S contains a disjunctive formula, say S = A⊃B, C_{1}, ..., C_{n}, then the result is immediate from the induction hypothesis applied to S′ = ¬A, B, C_{1}, ..., C_{n}, using ⊃-right.

Now we assume that S = Γ ∪ Π ∪ Σ, where Γ contains only negations of atoms, Π only atoms and Σ only conjunctive formulas.

Case 1. The case of two atoms in S connected by P corresponds to an Axiom, possibly followed by a sequence of Weakenings.

Now we assume that P ↦ C, for some conjunctive subformula C.

Case 2. There is a conjunctive formula X, in Σ, say X = ¬(A_{1}∨A_{2}), such that for every (P, P′) ∈ P, if P ≺ A_{i}, then also P′ ≺ A_{i}, say i = 2.

By condition (β) on P, the inductive hypothesis is satisfied by the proof structures ((¬A_{1}, Φ_{1})^{≺}, P_{1}) and (¬A_{2}^{≺}, P_{2}). Here Φ_{1} is S \{X} and where the path P_{1} is P restricted to (A_{1}, Φ_{1})^{≺} and P_{2} is P restricted to A_{2}^{≺}. Therefore ⊢ ¬A_{1}, Φ_{1} and ⊢ ¬A_{2} are derivable. The claim follows by ∨-left.

Case 3. There is a conjunctive formula X in Σ, say X = ¬(A⊃B), such that one immediate subformula, say ¬B, is connected only to Π ∪ Γ.

Let Γ_{1}, Π_{1} be the list of atoms or negations of atoms in S connected to ¬B and let Γ_{0} = Γ \ Γ_{1}, Π_{0} = Π \ Π_{1}, Σ_{0} = Σ \ {X}. By definition of path (4.2.(a)), these lists are disjoint. The inductive hypothesis holds again for (Γ_{1} ∪ Π_{1} ∪ {¬B})^{≺}, on one hand, and (Γ_{0} ∪ Π_{0} ∪ Σ_{0})^{≺}, on the other, with the set P appropriately restricted. Our claim follows by ⊃-left.

Case 4. none of the above.

Now P ↦ C, for some (conjunctive) subformula C ∈ Σ, and since cases 2 and 3 do not apply, for each X ∈ Σ there is a (conjunctive) Y ∈ Σ such that ...−X −Y. Let Chain be the set of all conjunctive chains on S. Thus Chain is nonempty, and it contains an infinite chain C^{∞}. Furthemore, Chain contains no terminal chain, since cases 2 and 3 do not apply.

Let X_{0} ∈ Σ be minimal with respect to ≫. Such a X_{0} exists by Lemma 2, say X_{0} = A_{1} ∧ A_{2}. For i = 1, 2 let

Σ_{i} = {Y ∈ Σ \ {X_{0}} : Y ∥ A_{i}
or A_{i} − C − Y, for some pure chain C with X_{0} ∉ C}.

Since there is no cycle and X_{0} is minimal with respect to ≫, †

Σ_{1} ∩ Σ_{2} = ∅

Let

Γ_{i} = {P ∈ Γ : P ∥ Σ_{i} ∪ {A_{i}}} Π_{i} = {P ∈ Π : P ∥ Σ_{i} ∪ {A_{i}}}

By the property (a) of paths,

Γ_{1} ∩ Γ_{2} = ∅ = Π_{1} ∩ Π_{2}

Let Φ_{i} = Γ_{i} ∪ Π_{i} ∪ Σ_{i} ∪ {A_{i}} and let

P_{i} = {(P, Q) ∈ P : for some Z, Z′ ∈ Φ_{i}, we have P ≺ Z and Q ≺ Z′}.

We would like to apply the induction hypothesis to (Φ_{i}, P_{i}) and then conclude by using ∧-right. We certainly can do so if we show that

For each i, P_{i} is a path for Φ_{i}.

The fact that the P_{i} are minimal and satisfy (α), (β) and (γ) follows immediately from the same fact for P.

Lemma 3. If Chain contains and infinite chain but no cycle, and X ∈ S, X ≠ X_{0}, then

X ∥ Y, Y ∈ Σ_{i} ∪ {A_{i}} ⇒ X ∈ Φ_{i}.

Proof. If X is atomic, then by definition X ∈ Γ ∪ Π. Suppose X is conjunctive and not X = A_{i}.

Let Y be A_{i}. Since in S, Chain has no terminal chain, certainly ... − X′ − X −_{A_{i}} X_{0}, i.e., X ∈ Σ, and thus X ∈ Σ_{i}.

† This is crucial: for a partition of Σ \ A∧B to exist, the conjunctive chains reaching out from A and B must not join, not only in a cycle but also in the exit of a loop: here we need the minimality condition.

Assume now that Y ∈ Σ_{i}, say Y ∈ Σ_{1} and, moreover, that X ∉ Σ_{1}. We show that this contradicts the assumption that P is a minimal path for S; we conclude that X ∈ Σ_{1}.

Fact. Let X, Y, Y′ be conjunctive, with Y′ ∥ Y ∥ X; suppose Y, Y′ ∈ Σ_{1} but X ∉ Σ_{1}. If C ∘ D ≺ Y is such that Y′ ∥ C and X ∥ D, then C ∘ D is disjunctive. Proof. Let A_{1} − C − Y′ − Y be a pure chain, where we may suppose that Y ⊀ Z for all Z ∈ C. If C ∘ D is conjunctive, then A_{1} − C − Y′ − C ∘ D − X is a pure chain, i.e., C ∈ Σ_{1}.

Returning to the refutation of the assumption X ∉ Σ_{1}, first notice that this implies X ∉ Σ_{2} too. Otherwise, given pure chains Y − C_{1} − A_{1} and A_{2} − C_{2} − X we conclude that Y − C_{1} − X_{0} − C_{2} − X − Y is a loop, thus X_{0} is not minimal with respect to ≫.

Now let Φ_{0} be S \ (Φ_{1} ∪ Φ_{2}). If U ∈ Φ_{0} and U ∥ V with V ∈ Φ_{j}, for j = 1, 2, then U and V are conjunctive. Let (Q, Q′) ∈ P be such that Q′ ≺ U and Q ≺ V. If A_{i} − … − V′ − V is any pure chain and (P, P′) is such that P′ ≺ V′ and P ≺ V, then there must be a disjunctive subformula C ∘ D of V such that, say, P ≺ C and Q ≺ D, by the above Fact. Therefore, if we drop (Q, Q′) from P, then the resulting path still satisfies the relevance condition on conjunctive subformulas, relatively to Σ_{j}. In conclusion, let

P_{0} = {(P, Q) ∈ P : for some Z ∈ Φ_{0}, P ≺ Z or Q ≺ Z}

and let

P′ = P \ P_{0}.

It is easy to check that P′ is a path not only for Φ_{1} ∪Φ_{2}, but also for S. But P′ is a proper subset of P, and this contradicts the minimality of the path P.

Now we can conclude the proof of the Theorem and check the conditions of Section 3.1. for P_{i}. Of these, (a) and (d) are immediate and (b) follows from relevance for A_{i} and Lemma 3.

We need to check the relevance condition (c). Assume P_{i} ↦ C∧D ≺ Φ_{i} via (P, P′), say P ≺ C and P, P′ ≺ Φ_{i}. Then there is a (Q, Q′) ∈ P such that P ↦ D via (Q, Q′), say Q ≺ D. Let X ∈ S such that Q′ ≺ X. Since C∧D ≺ Φ_{i}, Lemma 3 implies that X ∈ Φ_{i}. This means that (Q, Q′) ∈ P_{i}, namely P_{i} ↦ D.

6. Equivalence with Girard’s Proof Nets

Of course, the equivalence of the decision procedure with Girard’s Proof Nets for the Multiplicative Fragment with box for Weakening follows from their equivalence with Sequent Calculus for Direct Logic. But there may be some interest in seeing a direct graph-theoretic proof.

Lemma. If β is a Proof-Net with conclusions S and without Cut-links in propositional Multiplicative Linear Logic without ⊥, 1, then there is a minimal path P for S satisfying conditions (α), (β) and (γ).

Proof. Let P be the set of axiom links of the Proof-Net β. Suppose P is not minimal, and let P′ be a proper subset of P and also a path for S. Then either (1) there is a proper subset S′ of S such that P′ ↛ S \ S′, or (2) there is a nonempty set of subformulas C ∘ D in β such that, say, P′ ↦ C and P′ ↛ D. In case (1) no trip starting in S′ will ever reach S \ S′. In case (2) “∘” in C ∘ D must be a “par”, since P′ satisfies the relevance condition for conjunctive subformulas. We obtain a short trip as follows: start with an X such that P′ ↦ X; if and when a trip reaches C downwards, continue the trip upwards on C, etc. Thus in both cases, we contradict the fact that β is a Proof-Net.

Suppose P does not satisfy condition (β). It is easy to see that to (S^{≺}, P) there corresponds a Girard proof structure of the form

Axiom

P_{1} P_{2} ... ...

(A B) / (A ⊗ B)

..........

Notice that the switches can always be arranged in such a way that from A^{∧} the trip reaches directly P_{1}^{∧} and from P_{2}_{∨} reaches directly B_{∨}. Then set the switch on L at the indicated times link: the trip

A^{∧}, ..., P_{1}^{∧}, P_{2}_{∨}, ..., B_{∨}, A^{∧}

never reaches A ⊗ B, and so is short.

Suppose P does not satisfy condition (γ). Then there is a Girard Proof Structure of the form

Axiom

Axiom  Axiom
. . . . .
P_{n}^{⊥}  P_{1}  P_{1}^{⊥}  P_{2}  P_{n−1}^{⊥}  P_{n}
. . . . . . . . . . .  . . . . . . . . . . .  . . . . . . . . . . . . . .
B_{1}  C_{1}  B_{2}  C_{2}  B_{n}  C_{n}
B_{1} ⊗ C_{1}  B_{2} ⊗ C_{2}  B_{n} ⊗ C_{n}
. . . . . . . . . . .  . . . . . . . . . . .  . . . . . . . . . . . . . .

Again we can set the switch to obtain a short trip:

B_{1}^{∧}, ..., P_{n}^{⊥}^{∧}, P_{n}_{∨}, ..., C_{n}_{∨}, B_{n}^{∧}, ..., C_{2}_{∨}, B_{2}^{∧}, ..., P_{1}^{⊥}^{∧}, P_{1}_{∨}, ..., C_{1}_{∨}, B_{1}^{∧}.

Lemma. If (S^{≺}, P) satisfies (α), (β) and (γ), then there is a Proof Net β (with boxes)

The proof follows that of Main Theorem (⇐): in Case 1 we construct a Proof Net consisting of just an axiom, possibly inside several boxes. In Cases 2, 3 the result is given by the induction hypothesis and in Case 4 Lemma 3 of 5.1 guarantees that we can split the structure and apply the induction hypothesis.

7. Implementation of the Decision Procedure for DPC

We shall sketch the definition of a decision procedure for Direct Predicate Calculus. No extensions – natural or not – will be discussed.

We may assume, for the sake of exposition, that we are considering a formula F involving only ∧, ∨, ¬ with all negations pushed in, Skolemized and all unifiable (existential) variables noted. As shown in an arbitrary formula can be gotten into this form by linear time transformations. Of course, the procedures defined below can be applied with minimal change to the more general case.

We will use symbols p, q, r, … to denote atoms or negated atoms, U, V, … for unifiers: unifiers are viewed as finite sequences of pairs (x, t), where x is a variable and t is term.

Let us define a match as a triple (p, q, U), where we have a a positively occurring term p together with a negatively occurring formula q with a unifier U such that

(M.a) : p[U] = q[U].

and

(M.b) : there is no conjunction A∧B such that p ≺ A and q ≺ B or vice versa. We will re-define the notion of a path slightly: A path is a finite sequence of matches

paired with a unifier containing all the unifiers in the matches such that (P.a) : no literal occurs more than once. We shall use symbols P, Q, R, … to denote paths, and symbols X, Y, … to denote

sets of paths.

We also need to define functions that combine paths:

(P, Q) returns the least path R containing all the matches in P and Q. If no such path exists, it returns . We will use the notation P ∗Q for the resulting path.

For any formula A and set of paths X, let X \ A be the set of paths in X containing no literals ≺ A.

7.1. The Goal

Our objective is to decide whether there exists a path P of matches such that

(a) P satisfies F (P ↦ F): there is a triple (p, q, U) in P such that p ≺ F or q ≺ F.

(b) if P ↦ A∧B, then P ↦ A and P ↦ B.

(c) P contains no cycles; there is no sequence A_{1} − A_{2} − … − A_{n} = A_{1} of distinct conjunctions appropriately connected to each other via conjunctive components. As we have shown, such paths correspond to proofs; our problem is equivalent to

finding a proof of F. Each element of such a path corresponds to an axiom in the sense of Gentzen calculi; a sequent of the form p → q.

Thus the critical issue consists of defining an appropriate search strategy for paths with all of the above properties. Note that the search space size is roughly exponential in size with respect to the size of F. Thus we need limit the search in smart ways.

7.2. Finding All Matches

The first phase of the process consist of finding the set M of all matches (p, q, U) that can occur in a path described above.

Let L be the set of all literals in F. Then L = POS∪NEG, the union of all positive and negative literals in F.

Construct the set of all such matches, M, by unifying each p in POS against each q in NEG s.t. condition (b) for matches is satisfied.

This process is roughly quadratic in the size of F. In practice, the use of suitable indexing methods will make this pass very fast.

Define a function on L as follows: For any p in L, (p) is the set of all matches associated to p in M:

(p) = {(p, q, U)| (p, q, U)∈M} (p∈POS),

or

(p) = {(q, p, U)| (q, p, U)∈M} (p∈NEG).

7.3. Simple Depth First Search

Let’s look at the problem of finding paths with (a) and (b): Any non-empty path P automatically satisfies (a). If (b) is not true, then the set

(P) = {A|A∧B ≺ F ∧P ↦ B∧¬P ↦ A}

is non-empty. For any A in this set, we can look at the set of all possible extensions to P:

(P, A) = {Q ∗ P|Q∈ (p), p ≺ A},

and then repeating this process for the members of this set until we have constructed a path with no uncovered conjuncts.

This allows us to find a path satisfying (a) and (b) without having to construct all alternatives at the same time. This can be time consuming, since the suggested algorithm will do an enormous amount of re-computation in situations where an entire branch terminates in failure or no proof exists. In fact, in a typical “first time around” situation the “fact” to be proved is often invalid — the user in question forgot to include all the relevant assumptions.

7.4. Breadth First Search: Pre-Computing Valid Path Combinations

The simplest algorithm using breadth first search can be expressed in terms of computing the function on all subformulas of F:

(p) = {{((q, r, U), U)}|(q, r, U)∈  (p)}  (p∈L)
(A∧B) = {P ∗ Q|P∈  (A), Q∈  (B)}
(A∨B) = (  (A) \ B)∪(  (B) \ A)∪
{P ∗ Q|P∈  (A) −  (A) \ B, Q∈  (B) −  (B) \ A}.

This, of course, has the effect of computing all possible proofs for F. (F) then results in all paths with properties (a) − (b). What remains is to find a non-cyclic path. More precisely, every valid path contains a path from (F).

Of course, the algorithm suggested by the above equations is impractical. We propose an alternative; an algorithm that combines aspects of depth and breadth first search in order to prune the search space down as much as possible.

7.5. Static Irrelevance Elimination: the First Refinement

One of the primary causes for failure is irrelevance; a subformula may have no connections with any other fact simply because some critical assumptions were omitted. Let’s call a subformula weakly irrelevant if none of its subformulas can occur as a subformula of an axiom in any Direct Predicate Calculus proof of F. In the language of Gentzen calculi, this means that the only way it can be introduced into a proof is through the rule of weakening. In practice, weak irrelevancy is hard to compute. Instead, it is better to return to our stated goals; namely reduction in the size of the search space for valid paths or proofs. One step towards this goal is to eliminate in advance those literals that provably cannot occur as a part of any valid path for the entire formula. We can make a few observations:

Lemma 1: If (p) is empty, then p cannot occur as a part of any valid path. Proof: Obvious.

Lemma 2: If no literal of a formula A occurs as a part of any valid path, then the same holds for any formula of the form A∧B.

Proof: If not, take a valid path P ↦ A∧B. But then P ↦ A by property (b) of paths.

Lemma 3: If all literals of (p) other than p cannot occur as a part of any valid path, then p cannot occur as a part of any valid path.

Proof: Obvious.

Definition The set of irrelevant formulas is the smallest set of formulas closed under the following rules:

• If (p) is empty or contains matches of p to only irrelevant literals, p is irrelevant.

• If A and B are irrelevant, then A∨B is irrelevant.

• If A or B is irrelevant, then A∧B is irrelevant.

• If A is irrelevant and B ≺ A, then B is irrelevant.

Theorem 4. No subliteral of an irrelevant formula cannot occur as a part of a valid path.

Proof: Obvious, from above.

It is useful to observe the interaction of the last two rules; if any part of a conjunction is irrelevant, then all other parts may be declared irrelevant. Irrelevancy elimination can be simply implemented as a relaxation algorithm; mark formulas irrelevant until no more irrelevance can be found.

In practice, irrelevance elimination significantly reduces the search space for valid paths: We may from now on assume that all literals in L are not irrelevant.

7.6. Modified Breadth First Search: Partial Pre-Computation

As pointed out above, a full breadth first algorithm is impractical; too much information is kept and computed. Our second improvement involves only partially computing the function on the set of all subformulas of F. First of all, we wish to separate all potential paths into strongly connected components; if F is conjunctive, they are the conjunctive components of F. Thus, in this case we apply our procedure separately to each component. We may assume that F is disjunctive, of the form C_{1}∨C_{2}∨ … C_{n}. In fact, we expect that in the most typical instance F represents a query of the form

A_{1}∧A_{2}∧ … ⊃B;

i.e., to conclude fact B from assumptions A_{1}, A_{2}, . . ..

We compute the function for all elements of Dom, the set of all disjunctive sub-components of F.

Given the function on Dom, we can extend our irrelevance algorithm: Remove from the set M all matches not occurring in any (A) for A∈Dom. Declare any A irrelevant for which (A) = 0. We can then apply the methods defined in the previous section iteratively in order to further reduce the search space.

7.7. Searching for Paths

We can now describe our algorithm in full: Consider the function on Dom, where

Dom = {C_{1}, C_{2}, ...., C_{n}},

such that

0 < card(  (C_{1}))≤card(  (C_{2}))≤ …

We search in order through Dom, trying to find an element of P∈ (C_{i}) that can be extended to a complete path. If no such path can be found in C_{i}, we declare the subformula C_{i} irrelevant, compute the propagated irrelevancies, and move onto the next element in Dom. If no such element in Dom can be found, we return failure.

The general step in completing a path is as follows: Consider a path P, and the set

(P) = {C∈Dom|P ↦ C, P contains no path from (C)}.

Pick a C in this set with the lowest index, and consider all extensions of P that are complete with respect to C:

(P, C) = {Q ∗ P|Q∈ (C)};

repeat this process for the members of this set until we have constructed a path with no uncovered elements of Dom. This method will search through all paths satisfying (a) and (b).

7.8. Dealing with Cycles

It remains to consider the issue of detecting cycles in paths; at first blush, this seems time-consuming and complicated. But again there are many situations where it is not necessary to perform such a check and by a relaxation algorithm we can extend these situations iteratively much further.

Let us call a subformula non-cyclic if it cannot possibly contribute to a cyclic path. We can make the following observations:

A atom is non-cyclic if it is not contained in any conjunction.

If a formula is non-cyclic, so are all of its subformulas.

A conjunctive formula C is non-cyclic if all but one of the conjuncts connected to a conjunction distinct from C is non-cyclic.

The iterative application of these rules drastically reduces our need for cycle checking. For any match (p, q, U) we construct the set of all possible triples (A, B, C) such that

A, B,C are non-cyclic conjuncts occurring as a part of a path because of this match; i.e. A −_{D} B_{E} − C with p ≺ D and q ≺ E or vice versa. These triples will be stored in a table.

Then, for any path P it remains to check all of the triples in this table that are active for this path and verify that there is no cycle; i.e. a sequence of active triples

(A_{1}, A_{2}, A_{3}), (A_{2}, A_{3}, A_{4}), …, (A_{n}, A_{n+1}, A_{1}), (A_{n+1}, A_{1}, A_{2}),

where no A_{i} is a subexpression of another A_{j} for j ≠ i. Note that n has to be ≥2 for such a cycle. This is easily accomplished by a depth first search through the table.

8. Bibliography

:

A.Avron, The Semantics and the Proof Theory of Linear Logic, Laboratory for Foundations of Computer Science, University of Edinburgh, ECS-LFCS-87-27. :

V. Danos and L. Regnier, the structure of multiplicatives, Archive for mathematical logic 29, pp. 181-203, 1989 :

B.Dreben and W.D.Goldfarb, Solvable Classes of Quantificational Formulas, Reading Mass. Addison-Wesley, 1979. :

J.Y.Girard, Linear Logic, Theoretical Computer Science 50 (1987). :

J.Y.Girard, Geometry of Interaction, preprint, including:

Towards a Geometry of Interaction, forthcoming in AMS Proceedings of the Conference “Category Theory and Computer Science”, Boulder, June 1987;

Quantifiers in Linear Logic, forthcoming in Proceedings of the Conference SILFS, Cesena, January 1987;

Multiplicatives, forthcoming in Rendiconti del seminario matematico dell’ Universitá e Politecnico di Torino, 1988;

Linear Logic and Parallelism, forthcoming in Proceedings of the School on “Semantics of Parallelism” held in IAC, Roma, September 1986. :

J.Y.Girard, Geometry of Interaction I, Interpretation of the System F, preprint, Équipe de Logique, UA 753 du CNRS mathématiques, Université Paris VII, October 1988. :

Jussi Ketonen and Richard Weyhrauch, A Decidable Fragment of Predicate Calculus Theoretical Computer Science 32 (1984) pp. 297-307 :

O.Ketonen, Untersuchungen zum Praedikatenkalkul, Ann. Acad. Sci. Fennicae Series A I, Mathematica-Physica 23, (Springer Berlin, 1944). :

Y.Lafont: From Linear Algebra to Linear Logic, preprint, Laboratoire d’Informatique, École Normale Supérieure, Paris, October 1988. :

H.Lewis: Complexity of Solvable Cases of the Decision Problem for the Predicate Calculus, in: Proceedings of the IEEE Symposium on “Foundations of Computer Science” (1978),35-47. :

Hiroakira Ono, Strucural Rules and a Logical Hierarchy, forthcoming in Proceedings of Heyting 1988 Conference, Plenum Press. :

D.Prawitz, Natural Deduction, A Proof Theoretical Study, Alwqvist and Wicksell, Stockholm, 1965. :

G.Sambin, Intuitionistic Formal Spaces and their Neighborhood, forthcoming in Proceeding of the Logic Colloquium 1988, Padua.

Contents

1.  Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . .  2

1.1. Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2. Sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.3. Relations with the Classical System . . . . . . . . . . . . . . . . . 7 1.4. Basic Proof Theory . . . . . . . . . . . . . . . . . . . . . . . . 8 2. Linear logic and Direct Predicate Calculus . . . . . . . . . . . . 9 2.1. Proof Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.2. Multiple Conclusion Natural Deduction . . . . . . . . . . . . . . . 12 2.3. Proof search in Sequent Calculi . . . . . . . . . . . . . . . . . . . 13 3. A Decision Procedure for Direct Predicate Logic . . . . . . . . 15 3.1. Paths . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.2. Chains . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 3.3. The Main Theorem . . . . . . . . . . . . . . . . . . . . . . . . 17 3.4. An Example . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 4. Some Properties of Graphs . . . . . . . . . . . . . . . . . . . 19 4.1. Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 4.2. Basic Properties of Chains . . . . . . . . . . . . . . . . . . . . . 20 5. Proof of the Main Theorem . . . . . . . . . . . . . . . . . . . 22 5.1. From Proofs to Chains . . . . . . . . . . . . . . . . . . . . . . . 22 5.2. From Chains to Proofs . . . . . . . . . . . . . . . . . . . . . . . 23 6. Equivalence with Girard’s Proof Nets . . . . . . . . . . . . . . 26 7. Implementation of the Decision Procedure for DPC . . . . . . . 28 7.1. The Goal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 7.2. Finding All Matches . . . . . . . . . . . . . . . . . . . . . . . . 29 7.3. Simple Depth First Search . . . . . . . . . . . . . . . . . . . . . 29 7.4. Breadth First Search: Pre-Computing Valid Path Combinations . . . . . 30 7.5. Static Irrelevance Elimination: the First Refinement . . . . . . . . . . 30 7.6. Modified Breadth First Search: Partial Pre-Computation . . . . . . . . 31 7.7. Searching for Paths . . . . . . . . . . . . . . . . . . . . . . . . 32 7.8. Dealing with Cycles . . . . . . . . . . . . . . . . . . . . . . . . 32 8. Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . 34