From QBFs to MALL and back via focussing: fragments of multiplicative additive linear logic for each level of the polynomial hierarchy
Anupam Das
TL;DR
This paper establishes a correspondence between fragments of multiplicative additive linear logic and each level of the polynomial hierarchy by leveraging focussed proof systems and encoding techniques.
Contribution
It introduces a method to extract polynomial hierarchy levels from focussed proof systems, refining the understanding of MALL and MALLw complexity.
Findings
Fragments of MALLw complete for each polynomial hierarchy level
Encoding QBF satisfiability within focussed proof systems
Refined focussing to account for deterministic proof search phases
Abstract
In this work we investigate how to extract alternating time bounds from 'focussed' proof systems. Our main result is the obtention of fragments of MALLw (MALL with weakening) complete for each level of the polynomial hierarchy. In one direction we encode QBF satisfiability and in the other we encode focussed proof search, and we show that the composition of the two encodings preserves quantifier alternation, yielding the required result. By carefully composing with well-known embeddings of MALLw into MALL, we obtain a similar delineation of MALL formulas, again carving out fragments complete for each level of the polynomial hierarchy. This refines the well-known results that both MALLw and MALL are PSPACE-complete. A key insight is that we have to refine the usual presentation of focussing to account for deterministic computations in proof search, which correspond to invertible rules…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Parallel Computing and Optimization Techniques
From QBFs to MALL and back via focussing
Anupam Das
University of Birmingham
Abstract.
In this work we investigate how to extract alternating time bounds from ‘focussed’ proof systems. Our main result is the obtention of fragments of ( with weakening) complete for each level of the polynomial hierarchy. In one direction we encode QBF satisfiability and in the other we encode focussed proof search, and we show that the composition of the two encodings preserves quantifier alternation, yielding the required result. By carefully composing with well-known embeddings of into , we obtain a similar delineation of formulas, again carving out fragments complete for each level of the polynomial hierarchy. This refines the well-known results that both and are -complete.
A key insight is that we have to refine the usual presentation of focussing to account for deterministic computations in proof search, which correspond to invertible rules that do not branch. This is so that we may more faithfully associate phases of focussed proof search to their alternating time complexity. This presentation seems to uncover further dualities at the level of proof search than usual presentations, so could be of further proof theoretic interest in its own right.
The author was supported by a Marie Skłodowska-Curie fellowship, ERC project 753431, while conducting this research.
1. Introduction and motivation
Proof search is one of the most general ways of deciding formulas of expressive logics, both automatically and interactively. In particular, proof systems can often be found to yield optimal decision algorithms, in terms of asymptotic complexity. To this end, we now know how to extract bounds for proof search in terms of various properties of the proof system at hand. For instance we may establish:
- •
nondeterministic time bounds via proof complexity, e.g. [CR79, Kra95, CN10];
- •
(non)deterministic space bounds via the depth of proofs or search spaces, and loop-checking, e.g. [BI03, HSZ96, Ono98];
- •
deterministic or co-nondeterministic time bounds via systems of invertible rules, see e.g. [TS96, NVPR08].
However, despite considerable progress in the field, there still remains a gap between the obtention of (co-)nondeterministic time bounds, such as or , and space bounds such as . Phrased differently, while we have many logics we know to be -complete (intuitionistic propositional logic, various modal logics, etc.), we have very little understanding of their fragments corresponding to subclasses of .
An alternative view of space complexity is in terms of alternating time complexity, where a Turing machine may have both existential (i.e. nondeterminstic) and universal (i.e. co-nondeterministic) branching states. In this way is known to be equivalent to alternating polynomial time [CKS81]. This naturally yields a hierarchy of classes delineated by the number of alternations permitted in an accepting run, known as the polynomial hierarchy () [Sto76], of which both and are special cases. An almost exact instantiation of this (in a non-uniform setting) is the QBF hierarchy, where formulae are distinguished by their number of quantifier alternations in prefix notation. This raises the following open-ended question:
Question 1**.**
How do we identify natural fragments of -complete logics complete for levels of the polynomial hierarchy? In particular, can proof theoretic methods help?
In previous work, [Das17], we considered this question for intuitionistic propositional logic, obtaining partial answers for certain expressive fragments. In this work we consider the case of multiplicative additive linear logic () [Gir87], and its affine variant which admits weakening (); both of these are often seen as the prototypical systems for since their inference rules constitute the abstract templates of terminating proof search. Indeed, both and are well-known to be -complete [LMSS90, LMSS92], results that are subsumed by this work.111The result for is not explicitly stated in [LMSS90, LMSS92], but it is a folklore result that follows from those methods. By considering a ‘focussed’ presentation of , we analyse proof search to identify classes of theorems belonging to each level of . To demonstrate the accuracy of this method, we also show that these classes are, in fact, complete for their respective levels, via encodings from true quantified Boolean formulas (QBFs) of appropriate quantifier complexity, cf. [CKS81].
The notion of focussing is a relatively recent development in structural proof theory that has emerged over the last 20-30 years, e.g. [And92, Lau02, LM09]. Focussed systems elegantly delineate the phases of invertible and non-invertible inferences in proofs, allowing the natural obtention of alternating time bounds for a logic. Furthermore, they significantly constrain the number of local choices available, resulting in reduced nondeterminism during proof search, while remaining complete. This result is known as the ‘focussing’ or ‘focalisation’ theorem. Such systems thus serve as a natural starting point for identifying fragments of -complete logics complete for levels of .
One shortfall of focussed systems is that, in their usual form, they do not make adequate consideration for deterministic computations, which correspond to invertible rules that do not branch, and so the natural measure of complexity there (‘decide depth’) can considerably overestimate the alternating time complexity of a theorem. In the worst case this can lead to rather degenerate bounds, exemplified in [Das17] where an encoding of in intuitionistic logic requires a linear decide depth, despite being -complete.222Indeed, a similar gross overestimation presents in this work if we had used decide depth as our measure of complexity, cf. Fig. 3. To deal with this issue [Das17] proposed a more controlled form of focussing called over-focussing, which allows deterministic steps within synchronous phases, but as noted there this method is not available in due to the context-splitting rule. Instead, in this work we retain the classical abstract notion of focussing, but split the usual invertible, or ‘asynchronous’, phase into a ‘deterministic’ phase, with non-branching invertible rules, and a ‘co-nondeterministic’ phase, with branching invertible rules. In this way, when expressing proof search as an alternating predicate, a quantifier needs only be introduced in a co-nondeterministic phase. It turns out that this adaptation suffices to obtain the tight bounds we are after.
This is an extended version of the conference paper Focussing, and the polynomial hierarchy [Das18] presented at IJCAR ’18. The main differences in this work are the following:
- •
More proof details are provided throughout, in particular for the various intermediate results of Sects. 4, 5 and 6.
- •
A whole new section, Sect. 7, is included which extends the main results of [Das18] to pure , i.e. without weakening.
- •
The exposition is generally expanded, with further commentary and insights throughout.
In general, Sects. 2-6 of [Das18] cover the same content as their respective sections in this work, although theorem numbers are different.
This paper is structured as follows. In Sect. 2 we present preliminaries on QBFs and alternating time complexity, and in Sect. 3 we present preliminaries on and focussing. In Sect. 4 we present an encoding of true QBFs into , tracking the association between quantifier complexity and alternation complexity of focussed proof search. In Sect. 5 we explain how provability predicates for focussed systems may be obtained as QBFs, with quantifier complexity calibrated appropriately with alternation complexity (the ‘focussing hierarchy’). In Sect. 6 we show how this measure of complexity can be feasibly approximated to yield a bona fide encoding of back into true QBFs. Furthermore, we show that the composition of the two encodings preserves quantifier complexity, thus yielding fragments of complete for each level of the polynomial hierarchy. Sect. 7 extends this approach to pure via carefully composing with a certain encoding of into . Finally, in Sect. 8 we give some concluding remarks and further perspectives on our presentation of focussing.
2. Preliminaries on logic and computational complexity
In this section we will recall some basic theory of Boolean logic, and its connections to alternating time complexity.
This section follows Sect. 2 of [Das18], except that we include constants (or ‘units’) for generality here, and we also include a presentation of ‘Boolean Truth Trees’ in Sect. 2.2.
2.1. Second-order Boolean logic
Quantified Boolean formulas (QBFs) are obtained from the language of classical propositional logic by adding ‘second-order’ quantifiers, varying over propositions. Formally, let us fix some set of propositional variables, written etc. QBFs, written etc., are generated as follows:
[TABLE]
We write and for the classical truth constants false and true respectively, so that they are not confused with the units from linear logic later.
The formula stands for the negation of , and all formulas we deal with will be in De Morgan normal form, i.e. with negation restricted to variables as in the grammar above. Nonetheless, we may sometimes write to denote the De Morgan dual of , generated by the following identities:
[TABLE]
A formula is closed (or a sentence) if all its variables are bound by a quantifier ( or ). We write for the number of occurrences of literals (i.e. or ) in .
An assignment is a function , here construed as a set in the usual way. We define the satisfaction relation between an assignment and a formula , written , in the usual way:
- •
.
- •
.
- •
if .
- •
if .
- •
if or .
- •
if and .
- •
if or .
- •
if and .
Definition 2** (Second-order Boolean logic).**
A QBF is satisfiable if there is some assignment such that . It is valid if for every assignment . If is closed, then we may simply say that it is true, written , when it is satisfiable and/or valid.
Second-order Boolean logic () is the set of true QBFs.
In practice, when dealing with a given formula , we will only need to consider assignments that contain variables occurring in . We will assume this later when we discuss predicates (or ‘languages’) computed by open QBFs.
We point out that, from the logical point of view, it suffices to work with only closed QBFs, with satisfiability recovered by prenexing quantifiers and validity recovered by prenexing quantifiers.
Definition 3** (QBF hierarchy).**
For we define the following classes:
- •
is the set of quantifier-free QBFs.
- •
and, if , then so is .
- •
and, if , then so is .
Notice that if and only if , by the definition of De Morgan duality.
We have only defined the classes above for ‘prenexed’ QBFs, i.e. with all quantifiers at the front. It is well known that any QBF is equivalent to such a formula. For this reason we will henceforth assume that any QBF we deal with is in prenex normal form. In this case we call its quantifier-free part, i.e. its largest quantifier-free subformula, the matrix.
2.2. Boolean Truth Trees
In this work we will not need to formally deal with any deduction system for , although we point out that there is a simple system whose proof search dynamics closely match quantifier complexity, e.g. studied in [Let02]. We will briefly present a simplified system in order to exemplify the connection with alternating time complexity.
Boolean Truth Trees (BTTs) are a proof system whose lines are closed prenexed QBFs. Its inference rules are as follows,
[TABLE]
where varies over true quantifier-free sentences, i.e. true -combinations of and . Note that we could have further broken down the rule into several local computation rules, but that is independent of the current analysis.
Example 4**.**
Temporarily write for the exclusive-or function, i.e. is true if either is true or is true but not both. The following is a BTT proving :
[TABLE]
Notice that a step is invertible, i.e. its conclusion is true just if every premiss is true. On the other hand, an existential formula is true just if some step applies. In this way we can describe the proof search process itself by some ‘alternating’ predicate whose matrix is just a truth-checker for quantifier-free sentences, a deterministic computation. It is not hard to see that the alternations between and in such a predicate will, in this case, match the quantifier complexity of the input formula, by inspection of the rules. In order to make all of this more precise, we will need to speak more formally about alternating predicates and alternating complexity.
2.3. Alternating time complexity
In computation we are used to the distinction between deterministic and nondeterministic computation. Intuitively, co-nondeterminism is just the ‘dual’ of nondeterminism: at the machine level it is captured by ‘nondeterministic’ Turing machines where every run is accepting, not just some run as in the case of usual nondeterminism. From here alternating Turing machines generalise both the nondeterministic and co-nondeterministic models by allowing both universally branching states and existentially branching states.
Intuitions aside, we will now introduce the necessary concepts assuming only a familiarity with deterministic and nondeterministic Turing machines and their complexity measures. The reader may find a comprehensive introduction to relevant machine models and complexity classes in [Pap94].
For a language of strings over some finite alphabet, we write for the class of languages accepted in polynomial time by some nondeterministic Turing machine which may, at any point, query in constant time whether some word is in or not. We extend this to classes of languages , writing for . We also write for the class of languages whose complements are in .
Definition 5** (Polynomial hierarchy, [Sto76]).**
We define the following classes:
- •
.
- •
.
- •
.
The polynomial hierarchy () is .
We may more naturally view the polynomial hierarchy as the bounded-quantifier-alternation fragments of QBFs we introduced earlier. For this we construe and as classes of finite languages, by associating with a QBF (with all free variables indicated) the class of (finite) assignments satisfying it. These assignments may themselves may be seen as binary strings of length which encode their characteristic functions in the usual way.
Definition 6** (Evaluation problems).**
Let be a set of QBFs. -evaluation is the problem of deciding, given a formula , with all free variables indicated, and an assignment , whether .
Theorem 7** (cf. [CKS81]).**
For , we have the following:
- (1)
-evaluation is -complete. 2. (2)
-evaluation is -complete.
Corollary 8**.**
For , we have the following:
- (1)
\{\varphi\in\Sigma^{q}_{k}:\text{\varphi is closed and true}\}* is -complete.* 2. (2)
\{\varphi\in\Pi^{q}_{k}:\text{\varphi is closed and true}\}* is -complete.*
Proof.
Membership is immediate from Thm. 7, evaluating under the assignment . For hardness, notice that we may always simplify a QBF under an assignment to a closed formula as follows: first, replace all free variable occurrences with if and otherwise. Now simply apply the following rewrite rules,
[TABLE]
3. Linear logic and proof search
Linear logic was introduced by Girard [Gir87] to decompose the mechanics of cut-elimination by means of different connectives. It naturally subsumes both classical and intuitionistic logic by various embeddings, and has furthermore been influential in the theoretical foundations of logic programming via the study of focussing, which constrains the level of nondeterminism in proof search, cf. [And92, DMS10, CMS08]. In this work we only consider the fragment multiplicative additive linear logic () and its version with ‘weakening’().
This section mostly follows Sect. 3 of [Das18], mainly differing in that we here include units in the formulation of and , for generality, and give some further proof details.
3.1. Multiplicative additive linear logic
For convenience, we work with the same set of variables that we used for QBFs. To distinguish them from QBFs, we use the metavariables etc. for formulas, generated as follows:
[TABLE]
are called multiplicative connectives, and are called additive connectives. Like for QBFs, we have restricted negation to the variables, thanks to De Morgan duality in . Again, we may write for the De Morgan dual of , which is generated similarly to the case of QBFs:
[TABLE]
Due to De Morgan duality, we will work only with ‘one-sided’ calculi for and , where all formulas occur to the right of the sequent arrow. This means we will have fewer cases to consider for formal proofs, although later we will also informally adopt a two-sided notation when it is convenient, cf. Rmk. 14.
Definition 9** ().**
A cedent, written etc., is a multiset of formulas, delimited by commas ‘,’, and a sequent is an expression .333We will often identify cedents and sequents, since we are in a one-sided setting. The system (cut-free) is given in Fig. 1. , a.k.a. affine , is defined in the same way, only with the rule and rule replaced by the following analogues:
[TABLE]
We have not included the ‘cut’ rule, thanks to cut-elimination for linear logic [Gir87]. We will only study cut-free proofs in this paper. Notice that, following the tradition in linear logic, we write ‘’ for the sequent arrow, though we point out that the deduction theorem does not actually hold w.r.t. linear implication. For the affine variant, we have simply built weakening into the initial steps, since it may always be permuted upwards in a proof:
Proposition 10** (Weakening admissibility).**
The following rule, called weakening, is admissible in :
[TABLE]
Proof.
This is a routine (and indeed well-known) argument by induction on the size of a subproof that roots a weakening step. The initial sequents of are already closed under weakening, and have the following inductive cases:
[TABLE]
3.2. (Multi-)focussed systems for proof search
Focussed systems for (and linear logic in general) have been widely studied [And92, Lau02, DMS10, CMS08]. The idea is to associate polarities to the connectives based on whether their introduction rule is invertible (negative) or their dual’s introduction rule is invertible (positive). Now bottom-up proof search can be organised in a manner where, once we have chosen a positive principal formula to decompose (the ‘focus’), we may continue to decompose its auxiliary formulas until the focus becomes negative. The main result herein is the completeness of such proof search strategies, known as the focussing theorem (a.k.a. the ‘focalisation theorem’).
It is known that ‘multi-focussed’ variants, where one may have many foci in parallel, lead to certain ‘canonical’ representations of proofs for [CMS08]. Furthermore, the alternation behaviour of focussed proof search can be understood via a game theoretic approach [DMS10]. However, such frameworks unfortunately fall short of characterising the alternating complexity of proof search in a faithful way. The issue is that the usual focussing methodology does not make any account for deterministic computations, which correspond to invertible rules that do not branch. Such rules are usually treated just like the other invertible rules, which in general comprise the ‘co-nondeterministic’ stages of proof search.
For these reasons we introduce a bespoke presentation of (multi-)focussing for , with a designated deterministic phase dedicated to invertible non-branching rules, in particular the rule. To avoid conflicts with more traditional presentations, we call the other two phases nondeterministic and co-nondeterministic rather than ‘synchronous’ and ‘asynchronous’ respectively. This terminology also reinforces the intended connections to computational complexity.
Henceforth we use etc. to vary over atomic formulas. We also use the following metavariables to vary over formulas with the indicated main connectives:
[TABLE]
‘Vectors’ are used to vary over multisets of associated formulas, e.g. varies over multisets of -formulas. We may sometimes view these as sequences or even sets for convenience. Sequents may now contain a single delimiter or .
Definition 11** (Multi-focussed proof system).**
We define the (multi-focussed) system in Fig. 2. The system is the same as but with the and rules replaced by the rules and from (2).
A proof of a formula is simply a proof of the sequent , i.e. there is no need to pre-decorate with arrows, as opposed to usual presentations, thanks to the deterministic phase. The rules and are called decide and co-decide respectively, while and are called release and co-release respectively.
Notice that the determinism of plays no role in this one-sided calculus, but in a two-sided calculus we would have a deterministic left rule that is analogous to the given rule (on the right). This is the same as how the ‘negativity’ (in the sense of non-invertibility on the left) of plays no role in this calculus. One may argue that a on the left is morally just a , but such a simplification sacrifices the duality of connectives being reflected in terms of duality in computational complexity: if is deterministic, then so should be its dual, . Indeed, in the above classification, -formulas are dual to -formulas, -formulas dual to -formulas, and -formulas dual to -formulas.
As usual for multi-focussed systems, the analogous focussed system can be recovered by restricting rules to only one focussed formula in nondeterministic phases. Moreover, in our presentation, we may also impose the dual restriction, that there is only one formula in ‘co-focus’ during a co-nondeterministic phase:
Definition 12** (Simply (co-)focussed subsystems).**
A proof is focussed if in is always a singleton. It is co-focussed if in is always a singleton. If a proof is both focussed and co-focussed then we say it is bi-focussed.
The notion of ‘co-focussing’ is not usually possible for (multi-)focussed systems since the invariant of being a singleton is not usually maintained in an asynchronous phase, due to the rule. However we treat as deterministic rather than co-nondeterministic, and we can see that the -rule indeed maintains the invariant of having just one formula on the right of .
Theorem 13** (Focussing theorem).**
We have the following:
- (1)
The class of bi-focussed -proofs is complete for . 2. (2)
The class of bi-focussed -proofs is complete for .
Evidently, this immediately means that (), as well as its focussed and co-focussed subsystems, are also complete for (resp. ). The proof of Thm. 13 follows routinely from any other completeness proof for focussed , e.g. [And92, Lau02]. The only change in our presentation is in the organisation of phases, for which we may think of bi-focussed proofs as certain annotated focussed proofs.
To aid our exposition, we will sometimes use a ‘two-sided’ notation and extra connectives so that the intended semantics of sequents are clearer. Strictly speaking, this is just a shorthand for one-sided sequents: the calculi defined in Figs. 1 and 2 are the formal systems we are studying.
Notation 14** (Two-sided notation).**
We write as shorthand for the sequent , where is . We extend this notation to sequents with or symbols in the natural way, writing for and for . In all cases, (co-)foci are always written to the right of or .
We write as shorthand for the formula , and as shorthand for the formula . Sometimes we will write, e.g., a step,
[TABLE]
which, by definition, corresponds to a correct application of in .
4. An encoding from to
In this section we present an encoding of true QBFs into . (We will later adapt this into an encoding into in Sect. 7.) The former were also used for the original proof that is -complete [LMSS90, LMSS92], though our encoding differs from theirs and leads to a more refined result, cf. Sect. 6.
This section mostly follows Sect. 4 from [Das18], except with some further details in proofs and the exposition. Henceforth we assume that all QBFs are in prenex normal form and free of truth constants and (e.g. by Eqn. 1).
4.1. Positive and negative encodings of quantifier-free evaluation
The base cases of our translation from QBFs to will be quantifier-free Boolean formula evaluation. This is naturally a deterministic computation, being polynomial-time computable. (In fact, Boolean formula evaluation is known to be -complete [Bus87].) However one issue is that this determinism cannot be seen from the point of view of , since the only deterministic connective (, on the right) is not expressive enough to encode evaluation.
Nonetheless we are able to circumvent this problem since is at least able to see that quantifier-free evaluation is in , via a pair of corresponding encodings. For non-base levels of this is morally the same as being deterministic, as we will see more formally over the course of this section.
Definition 15** (Positive and negative encodings).**
Let be a quantifier-free Boolean formula. We define:
- •
is the result of replacing every in by and every in by .
- •
is the result of replacing every in by and every in by .
For an assignment and a list of variables , we write for the cedent . We write for the cedent consisting of copies of each literal in .
Proposition 16**.**
Let be a quantifier-free Boolean formula with free variables and let be an assignment. For , the following are equivalent:
- (1)
. 2. (2)
* proves .* 3. (3)
* proves .*
Proof.
21 and 31 are immediate from the ‘soundness’ of with respect to classical logic, by interpreting or as and or as .
Intuitively, 12 follows directly from the invertibility of rules, while for 13 we may appeal to the usual properties of satisfaction while controlling linearity appropriately. Formally we prove the following more general statements:
- •
For any multiset of quantifier-free Boolean formulas, if then proves , where is the cedent .
- •
For any quantifier-free Boolean formula with , if then proves .
We proceed by induction on the number of connectives in or . The bases case is simple (relying on affinity) and the inductive cases are as follows,
[TABLE]
where:
- •
or , depending on whether or , respectively; and,
- •
and are chosen so that and ; and,
- •
the derivations marked are obtained from the inductive hypothesis.∎
4.2. Encoding quantifiers in
As we said before, we do not follow the ‘locks-and-keys’ approach of [LMSS90, LMSS92]. Instead we follow a similar approach to Statman’s proof that intuitionistic propositional logic is -hard [Sta79], adapted to minimise proof search complexity.
The basic idea is that we would like to encode quantifiers as follows:
[TABLE]
The issue is that such a naive approach would induce an exponential blowup, due to the two occurrences of in each line above. This idea was considered by Statman in [Sta79], for intuitionistic propositional logic, where he avoided the blowup by using Tseitin extension variables, essentially fresh variables used to abbreviate complex formulas, e.g. . The issue is that this can considerably complicate the structure of proofs, since, in order to access the abbreviated formula, we must pass both a positive and negative phase induced by .
Instead, we use an observation from [Das17] that occurs only positively in (3) above, and so we only need one direction of Tseitin extension. Doing this carefully will allow us to control the structure proofs in a way that is consistent with the alternation complexity of the initial QBF, as we will see later.
Definition 17** ( to ).**
Given a QBF with and all quantifiers indicated, we define by induction on as follows,
[TABLE]
where is always fresh.
Lemma 18**.**
Let be a QBF with all free variables displayed and matrix , with . Then if and only if proves for any assignment and any disjoint from .
Proof.
We proceed by induction on the number of quantifiers in . For the base case, when is quantifier-free, we appeal to Prop. 16. The left-right direction follows directly by weakening (cf. Prop. 10), while the right-left direction follows after observing that does not occur in or ; thus may be deleted from a proof (along with its descendants) while preserving correctness.
For the inductive step, in the left-right direction we give appropriate bi-focussed proofs in Figs. 3 and 4, where: in Fig. 3 is chosen to be if and otherwise; the derivations marked are obtained by the inductive hypothesis; and the derivation marked in Fig. 4 is analogous to the one on the left of it.444Note that, for the derivations for the innermost quantifier ( or ), the topmost or step of Figs. 3 or 4 (resp.) does not occur.
For the right-left direction, we need only consider the other possibilities that could occur during bi-focussed proof search, by the focussing theorem, Thm. 13. For the case, bottom-up, one could have chosen to first decide on in the antecedent. The associated step would have to send the formula to the right premiss (for ), since otherwise every variable occurrence in that premiss would be distinct and there would be no way to correctly finish proof search. Thus, possibly after weakening, we may apply the inductive hypothesis to the left premiss (for ). A similar analysis of the upper step in Fig. 3 means that any other split will allow us to appeal to the inductive hypothesis after weakening. For the case the argument is much simpler, since no matter which order we ‘co-decide’, we will end up with the same leaves. (This is actually exemplary of the more general phenomenon that invertible phases of rules are ‘confluent’, cf. [And92, CMS08, LM09].) In particular, -steps may be permuted as follows:
[TABLE]
Theorem 19**.**
A closed QBF is true if and only if proves .
Proof.
Follows immediately from Lemma 18, setting . ∎
5. Focussed proof search as alternating time predicates
In this section we show how to express focussed proof search as an alternating polynomial-time predicate that will later allow us to calibrate the complexity of proof search with levels of the QBF and polynomial hierarchies. The notions we develop apply equally to either or .
This section mostly follows Sect. 5 of [Das18] except that, as well as further general details, we include a proof of Theorem 21 (essentially Theorem 20 in [Das18]).
We will now introduce ‘provability predicates’ that delineate the complexity of proof search in a similar way to the QBF and polynomial hierarchies we presented earlier. Recall the notions of deterministic, nondeterministic and co-nondeterministic rules from Dfn. 11, cf. Fig. 2.
Definition 20** (Focussing hierarchy).**
A cedent of is:
- •
-provable, equivalently -provable, if is provable using only deterministic rules.
- •
-provable if there is a derivation of , using only deterministic and nondeterministic rules, from sequents which are -provable.
- •
-provable if every maximal path from , bottom-up, through deterministic and co-nondeterministic rules ends at a -provable sequent.
We sometimes simply say “ is ” or even “” if is -provable.
The definition above is robust under the choice of multi-focussed, (co-)focussed or bi-focussed proof systems: while the number of or steps may increase, the number of alternations of nondeterministic and co-nondeterministic phases is the same. This robustness will also apply to other concepts introduced in this section.
From the definition it is not hard to see that we have a natural correspondence between the focussing hierarchy and the other hierarchies we have discussed:
Theorem 21**.**
For , we have the following:
- (1)
-provability is computable in . 2. (2)
-provability is computable in .
An analogous result has been presented in previous work, [Das17]. An interesting point is that, for the rule, even though there are two premisses, the rule is context-splitting, and so a nondeterministic machine may simply split into two parallel threads with no blowup in complexity.
of Thm. 21.
We proceed by induction on . In the base case, a cedent is -provable (equivalently -provable) just if it has a proof using only deterministic rules. Upon inspection of Fig. 2, we notice that it does not matter which order we apply deterministic rules, bottom-up, since maximal application will always lead to the same sequent at the top. This follows from a simple rule permutation argument:
[TABLE]
Thus, since deterministic rules must terminate after a linear number of steps (bottom-up), we may verify deterministic-provability by simply applying deterministic steps maximally (in any order bottom-up) and verifying that the end result is a correct initial sequent. Thus we indeed have that -provability (equivalently -provability) is computable in .
For the inductive step for 1, a cedent is not -provable just if there is some maximal branch of co-nondeterministic steps applied to , bottom-up, that terminates in a sequent that is not -provable. Any such branch has polynomial-size (by inspection of the rules), and we have from the inductive hypothesis that -provability is computable in . Thus we have that non--provability is computable in and so, by Dfn. 5, -provability is computable in .
For the inductive step for 2, a cedent is -provable just if there is a derivation of the form,
[TABLE]
using only deterministic and nondeterministic rules such that each is -provable. Notice that such has polynomial-size in with , by inspection of the (non)determinstic rules in Fig. 2. Thus, to check that is -provable we need only guess the appropriate derivation and sequents , and then check that each is -provable. By the inductive hypothesis, we have that -provability is a property, so we may check on a -machine that all these s are actually -provable in time . Thus we have that -provability is indeed computable in . ∎
Corollary 22**.**
For , we have the following:
- (1)
There are formulas , constructible in time polynomial in , computing -provability on all formulas s.t. . 2. (2)
There are formulas , constructible in time polynomial in , computing -provability on formulas s.t. .
Proof.
Follows immediately from Theorem 21 under Theorem 7. ∎
We now give a slightly different way to view the focussing hierarchy, based on a more directly calculable measure of cedents that is similar to the notions of ‘decide depth’ and ‘release depth’ found in other works, e.g. [Nig07]. We will use (a variation of) this to eventually formulate our encoding from to in the next section.
Definition 23** ((Co-)nondeterministic complexity).**
Let be a proof. We define the following:
- •
The nondeterministic complexity of , written , is the maximum number of alternations, bottom-up, between and steps in a branch through , setting if has only steps.
- •
The co-nondeterministic complexity of , written , maximum number of alternations, bottom-up, between and steps in a branch through , setting if has only steps.
For a cedent we further define the following:
- •
is the least s.t. there is a proof of with .
- •
) is the least s.t. there is a proof of with .
Putting together the results and notions of this section, we have:
Proposition 24**.**
Let be a cedent and . We have the following:
- (1)
* is -provable if and only if .* 2. (2)
* is -provable if and only if .*
6. An ‘inverse’ encoding from into
In this section we will use the ideas of the previous section to give an explicit encoding from to , i.e. a polynomial-time mapping from -formulas to QBFs whose restriction to theorems has image in . Moreover, we will show that this encoding acts as an ‘inverse’ to the one we gave in Sect. 4, and finally identify natural fragments of complete for each level of .
This section mostly follows Sect. 6 of [Das18], except that we give significantly more proof details.
6.1. Approximating (co-)nondeterministic complexity
The nondeterministic and co-nondeterministic complexities and we introduced in the previous section do not give us a bona fide encoding from to true QBFs since they are hard to compute. Instead we give an ‘overestimate’ here that will suffice for the encodings we are after. This overestimate will be parametrised by some enumeration of all formulas,555Strictly speaking, we really mean ‘formula occurrences’ rather than just ‘formulas’, but we will sweep this technicality under the carpet in the interest of a lighter exposition. which will drive the possible choices during proof search. However we will later show that the choice of this enumeration is irrelevant, meaning that the approximation can be flexibly calculated and is in fact polynomial-time computable.
Another option might have been, rather than taking the ‘least’ formula in a sequent under some enumeration, that we may view the sequent as a list instead in a calculus with an exchange rule. We avoided this in the interest of having a terminating proof system.
Throughout, we will identify enumerations with total orders in the natural way.
Definition 25** (Approximating the complexity of a sequent).**
Let be a total order on all formulas. We define the functions and on sequents in Fig. 5.666In the conference version, [Das18], there was an error in the base case, where [math] was written instead of .
Proposition 26** (Confluence).**
For any two total orders and on formulas, we have that and .
To prove this, we give essentially a confluence argument for terminating relations, but we avoid using a formal rewriting argument for self-containedness.
of Prop. 26.
We proceed by induction on the number of connectives in . The base case, when consists of only atomic formulas, is trivial, so we consider the inductive steps. When invoking the inductive hypothesis, we may freely suppress the subscripts or .
Suppose that, at some point along the definition of the approximations, and disagree on what the least formula is. Namely, the -least formula is and the -least formula is . In this case we have the following situation:
[TABLE]
where each is either or [math] depending on whether a co-nondeterministic phase is entered or not during the bi-pole induced by . We will have a similar derivation for , with only and swapped, whence we conclude by commutativity and associativity of addition.
The case where a -formula is chosen in the definition of is similar.
∎
From now on, we may suppress the subscript for the notions and .
Corollary 27** (Overapproximation).**
* and .*
Proof.
A proof with the minimal number of alternations between nondeterministic and co-nondeterministic phases will induce a strategy on which we may evaluate and . These will be bounded below by their actual and values. ∎
Notice that the over-estimation for the case is particularly extreme: in the worst case we have that the entire context is copied to one branch. In fact we could optimise this somewhat, by only considering ‘plausible’ splittings, but it will not be necessary for our purposes.
Corollary 28** (Feasibility).**
* and are polynomial-time computable.*
Proof.
Clearly, and are polynomial-time computable for any polynomial-time enumeration . So we may simply pick any polynomial-time enumeration of the formulas and appeal to Prop. 26. ∎
6.2. Tightness of approximations in the image of
Since is always a relatively ‘balanced’ formula, we have that the overestimation just defined is in fact tight in the image of from :
Proposition 29** (Tightness).**
For we have the following:
- (1)
If then and . 2. (2)
If then and .
Intuitively, the tightness of the approximation follows from the following two properties of the derivations in Figs. 3 and 4:
- •
There is only one non-atomic formula per sequent, so the -overapproximation is not significant.
- •
Weakening is only required on atomic formulas, so initial sequents need not be further broken down in the definitions of and .
of Prop. 29.
We have that and already from the proof of Lemma 18, so it remains to show that the approximations are tight. For this we show by induction on the number of quantifiers in or that, more generally:
- •
for any sequence of atomic formulas.
- •
for any sequence of atomic formulas.
When and are quantifier-free, notice that , since has only positive connectives and has only negative connectives.
If is then , for any , by the inductive hypothesis so:
[TABLE]
We also have that , by a similar analysis.
If is then , for any , by the inductive hypothesis so:
[TABLE]
We also have that , by a similar analysis. ∎
6.3. An encoding from to QBFs and main results
From Cor. 22, let us henceforth fix appropriate QBFs and , for , computing -provability and -provability in , respectively, for formulas of size . We are now ready to define our ‘inverse’ encoding of :
Definition 30** ( to ).**
For a formula , we define:
[TABLE]
Finally, we are able to present our main result:
Theorem 31**.**
We have the following:
- (1)
* is a polynomial-time encoding from to .* 2. (2)
* is a polynomial-time encoding from to .* 3. (3)
The composition preserves quantifier complexity, i.e., for , it maps true () sentences to true (resp. ) sentences.
Proof.
We already proved 1 in Thm. 19. 2 follows from the definitions of and (cf. Cor. 22), under Prop. 24 and Cors. 27 and 28. Finally 3 then follows by tightness of the approximations , in the image of , Prop. 29. ∎
Consequently, we may identify polynomial-time recognisable subsets of -formulas whose theorems are complete for levels of the polynomial hierarchy:
Corollary 32**.**
We have the following, for :
- (1)
\{A:\text{\lceil\sigma\rceil(A)\leq k\mathsf{MALL}\mathsf{w}A}\}* is -complete.* 2. (2)
\{A:\text{\lceil\pi\rceil(A)\leq k\mathsf{MALL}\mathsf{w}A}\}* is -complete.*
7. Extending the approach to (non-affine)
It is natural to wonder whether a similar result to Thm. 31 could be obtained for , i.e. without weakening. The reason we chose is that it allows for a robust and uniform approach that highlights the capacity of focussed systems to obtain tight alternating time bounds for logics, without too many extraneous technicalities. However, the same approach does indeed extend to with only local adaptations. We give the argument in this section.
This section is comprised of new material not present in [Das18].
7.1. Encoding weakening in
There is a well-known embedding of into by recursively replacing every subformula by . However, doing this might considerably increase the alternation complexity of proof search, adding up to one alternation per subformula. Instead, we notice that we need only conduct this replacement on literals, since those are the only ones that are weakened in the proofs of Sect. 4. From here we realise that the consideration of formulae of the form (or variants thereof) may be delayed to the end of proof search. To formalise this appropriately, we first need the following notion:
Definition 33** (Weakened formulas).**
Let be a proof whose initial -sequents are and initial -sequents are The weakened formulas of is the set .
We identify elements of in the above definition with subformula occurrences of the conclusion of in the natural way. We have the following folklore result:
Lemma 34** (Weakening lemma).**
*We have the following: *
- (1)
* proves .* 2. (2)
* proves , with weakening only on .* 3. (3)
Let be a formula and a set of subformula occurrences of . There is a proof of with weakened formulas among if and only if proves .
Proof.
1 and 2 are given by the following derivations:
[TABLE]
3 now follows immediately from 1 and 2 under the ‘deep inference’ property:
[TABLE]
This property is well known (see, e.g., [Str02]) and follows by a routine induction on the structure of , in particular appealing to the cut-elimination property of . For instance here are the cases when is a or formula,
[TABLE]
[TABLE]
where the derivations marked are obtained from the inductive hypothesis. The cases when is a or formula are similar to the two cases above. ∎
7.2. Adapting the translation for
It turns out that, in the arguments of Sect. 4, we only used weakenings on atomic formulae: notice that, in the proofs of Prop. 16 and of Lemma 18, the only weakenings were applied on literals, and all initial sequents had the form .
Observation 35**.**
The proof of Thm. 19 requires weakening only on literals.
This motivates the following definition:
Definition 36**.**
For a formula , write for the result of replacing every literal occurrence with .
We now have the following immediately from Lemma 34:
Proposition 37**.**
* proves if and only if proves .*
7.3. Dealing with formulas deterministically
Even though we have restricted our treatment of weakened formulas to only literals, these may still a priori increase the alternation complexity of proof search linearly under the encoding . To avoid this, we will work in a certain normal form of proofs that delays consideration of formulas of the form until the end of bottom-up proof search. To enforce this we must slightly ‘hack’ the proof systems and complexity approximations previously introduced.
For generality, let us introduce new metavariables etc. varying over -clauses containing at least one :
[TABLE]
Our intention is to treat -formulas much like atoms in proof search, in particular not decomposing them until the end. To this end, we will introduce a new focussed system that enforces this within the rules.
Definition 38** ().**
We temporarily redefine the metavariables so that only is permitted to vary over -formulas,i.e. if or is a -formula it must not be a -formula. The proof system is hence defined just as in Fig. 2, under this revision of metavariables, with the following exceptions:
- •
in Fig. 2 is everywhere replaced by , i.e. has the following rules,
[TABLE]
instead of their analogous versions written in Fig. 2.
- •
has the following additional initial sequents:
[TABLE]
where literals in parentheses must occur in their respective formulas. These new initial sequents are deterministic.
(Co-)focussed and bi-focussed proofs of are defined analogously to Dfn. 12.
Proposition 39**.**
(Bi-focussed) is sound and complete for .
Proof.
Soundness is routine, with the new initial sequents proved using simple and steps, along with the other initial rules.
For completeness, we proceed by induction on the size of a proof, by essentially a rule permutation argument. The critical cases are when a proof focusses on a -formula, which we adapt as follows:
[TABLE]
where,
- •
is obtained from by inductively adding to each premiss of an inference step in , bottom-up, except at steps where we must only add to one premiss, say the left one. This transformation preserves the local correctness of the proof, in particular since initial sequents are closed under addition of -formulas.
- •
is a literal and is obtained from by replacing every (indicated) occurrence of by . Since contains as a subformula, each initial sequent transformed in this way will again be an initial sequent.
All other cases are routine, simply mimicking the given proof. ∎
7.4. Adapting the translation and main results
Finally we adapt the approximations of (co-)nondeterministic complexity to reflect the proof search dynamics of :
Definition 40** (Approximating alternating complexity in ).**
and are defined exactly as and in Fig. 5, under the metavariable conventions of Dfn. 38, with the following exception: and are replaced everywhere by and “ or ”, respectively. I.e. we have the following clauses,
[TABLE]
instead of their analogous versions written in Fig. 5.
It is not hard to see that the results of Sect. 5 are applicable also to the notions and developed here. In particular Prop. 26 holds also for and and we may similarly omit the -subscript henceforth. All together, this allows us to define a similar encoding from formulas to QBFs.
First, appealing to Cor. 22,777Notice that this holds also for the system . let us henceforth fix appropriate QBFs and , for , computing -provability and -provability in , respectively, for formulas of size .
Definition 41** ( to ).**
For a formula , we define:
[TABLE]
We now have the following analogues of the main results of the previous section, proved by essentially the same arguments:
Theorem 42**.**
We have the following:
- (1)
* is a polynomial-time encoding from to .* 2. (2)
* is a polynomial-time encoding from to .* 3. (3)
The composition preserves quantifier complexity, i.e. for , it maps true () sentences to true (resp. ) sentences.
Corollary 43**.**
We have the following, for :
- (1)
\{A:\text{\lceil\sigma\rceil^{\prime}(A)\leq k\mathsf{MALL}A}\}* is -complete.* 2. (2)
\{A:\text{\lceil\pi\rceil^{\prime}(A)\leq k\mathsf{MALL}A}\}* is -complete.*
8. Conclusions and further remarks
We gave a refined presentation of (multi-)focussed systems for multiplicative-additive linear logic, and its affine variant, that accounts for deterministic computations in proof search, cf. Sect. 3. We showed that it admits rather controlled normal forms in the form of bi-focussed proofs, and highlighted a duality between focussing and ‘co-focussing’ that emerges thanks to this presentation. The main reason for using focussed systems such as ours was to better reflect the alternating time complexity of bottom-up proof search, cf. Sect. 5. We justified the accuracy of these bounds by showing that natural measures of proof search complexity for tightly delineate the theorems of according to associated levels of the polynomial hierarchy, cf. Sects. 4 and 6. We were also able to obtain a similar delineation for too, cf. Sect. 7. These results exemplify how the capacity of proof search to provide optimal decision procedures for logics extends to important subclasses of . As far as we know, this is the first time such an investigation has been carried out.
Our presentation of should extend to logics with quantifiers and exponentials, following traditional approaches to focussed linear logic, cf. [And92, Lau02]. It would be interesting to see what could be said about the complexity of proof search for such logics. For instance, the usual rule becomes deterministic in our analysis, since it does not branch:
[TABLE]
As a result, the alternation complexity of proof search is not affected by the -rule, but rather interactions between positive connectives, including , and negative connectives such as . Interpreting this over a classical setting could even give us new ways to delineate true QBFs according to the polynomial hierarchy, determined by the alternation of and propositional connectives rather than . One issue here is that witnessing steps seems to significantly impact the complexity proof search. Nonetheless this would be an interesting line of future research.
Much of the literature on logical frameworks via focussed systems is based around the idea that an inference rule may be simulated by a ‘bi-pole’, i.e. a single alternation between an invertible and non-invertible phase of inference steps. However accounting for determinism might yield more refined simulations where, say, non-invertible rules are simulated by phases of deterministic and nondeterministic rules, but not co-nondeterministic ones. In particular this should be possible for standard translations between modal logic and first-order logic, cf. [MV15, MMV16].
Acknowledgements
I would like to thank Taus Brock-Nannestad, Kaustuv Chaudhuri, Sonia Marin and Dale Miller for many fruitful discussions about focussing, in particular on the presentation of it herein. I am particularly grateful to Sonia Marin and the anonymous reviewers of both this work and the previous conference version, [Das18], for their careful and helpful proofreading.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[And 92] Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. Log. Comput. , 2(3):297–347, 1992.
- 2[BI 03] Samuel R Buss and Rosalie Iemhoff. The depth of intuitionistic cut free proofs, 2003. Preprint. http://www.phil.uu.nl/~iemhoff/Mijn/Papers/dpth IPC.pdf .
- 3[Bus 87] Samuel R. Buss. The Boolean formula value problem is in ALOGTIME. In Proceedings of the 19th Annual ACM Symposium on Theory of Computing (STOC) , 1987.
- 4[CKS 81] Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. J. ACM , 28(1):114–133, 1981.
- 5[CMS 08] Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin. Canonical sequent proofs via multi-focusing. In 5th International Conference On Theoretical Computer Science (TCS) , 2008.
- 6[CN 10] Stephen Cook and Phuong Nguyen. Logical Foundations of Proof Complexity . Cambridge University Press, New York, NY, USA, 1st edition, 2010.
- 7[CR 79] Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic , 44(1):36–50, 1979.
- 8[Das 17] Anupam Das. Alternating time bounds from variants of focussed proof systems, 2017. Submitted. http://anupamdas.com/alt-time-bnds-var-foc-sys.pdf .