A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic
Simon Docherty, Reuben N. S. Rowe
TL;DR
This paper introduces a novel infinitary labelled sequent calculus for propositional dynamic logic (PDL), providing soundness, completeness, and cut-free proof systems, along with proof-search strategies for specific PDL fragments.
Contribution
It presents a new non-wellfounded, labelled proof system for PDL, including a cyclic system that is finitely representable and proven to be sound and complete.
Findings
Both systems are sound and complete with respect to standard models.
The cyclic system G3PDL^{} is cut-free complete.
Proof-search strategies are developed for the fragment of PDL without tests.
Abstract
We define a infinitary labelled sequent calculus for PDL, G3PDL^{\infty}. A finitarily representable cyclic system, G3PDL^{\omega}, is then given. We show that both are sound and complete with respect to standard models of PDL and, further, that G3PDL^{\infty} is cut-free complete. We additionally investigate proof-search strategies in the cyclic system for the fragment of PDL without tests.
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.
11institutetext: Department of Computer Science, University College London, UK [email protected] 22institutetext: School of Computing, University of Kent, Canterbury, UK [email protected]
A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic
Simon Docherty and Reuben N. S. Rowe 1122
Abstract
We define an infinitary labelled sequent calculus for PDL, . A finitarily representable cyclic system, , is then given. We show that both are sound and complete with respect to standard models of PDL and, further, that is cut-free complete. We additionally investigate proof-search strategies in the cyclic system for the fragment of PDL without tests.
1 Introduction
Fischer and Ladner’s Propositional Dynamic Logic (PDL) [12], which is the propositional variant of Pratt’s Dynamic Logic [32], is perhaps the quintessential modal logic of action. While (P)DL arose initially as a modal logic for reasoning about program execution its impact as a formalism for extending ‘static’ logical systems with ‘dynamics’ via composite actions [20, p. 498] has been felt broadly across logic. This is witnessed in extensions and variants designed for reasoning about games [29], natural language [19], cyber-physical systems [31], epistemic agents [17], XML [1], and knowledge representation [10], among others.
What is lacking, however, is a uniform proof theory for PDL-type logics. Much of the proof theoretic work on these logics focuses on Hilbert-style axiomatisations, which are not amenable to automation. Proof systems for PDL itself can broadly be characterised as one of two sorts. Falling into the first category are a multitude of infinitary systems [33, 22, 14] employing either infinitely-wide -proof rules, or (equivalently) allowing countably infinite contexts. In the other category are tableau-based algorithms for deciding PDL-satisfiability [16, 18]. While these are (neccessarily) finitary, they require a great deal of auxillary structure tailored to the decision procedure for PDL itself, and it is unclear how they might be generalised to systems for variants or extensions of the logic.
In the proof theory of modal logic, a high degree of uniformity and modularity has been achieved through labelled systems. The idea of using labels as syntactic representatives of Kripke models in modal logic proof systems can be traced back to Fitting [13], and a succinct history of the use of labelled systems is provided by Negri [27]. Negri’s work [26] is the high point of the technique, giving a procedure to transform frame conditions for Kripke models into labelled sequent calculi rules preserving structural properties of the proof system, given they are defined as coherent axioms.
The power of this rule generation technique is of particular interest because it enables the specification of sound and complete systems for classes of Kripke frames that are first-order, but not modally, definable. In the context of PDL-type logics, this is of interest because of common additional program constructs like intersection which have a non-modally definable intended interpretation [30]. However, even with this expressive power, such a framework on its own cannot account for program modalities involving iteration. In short, formulae involving these modalities are interpreted via the reflexive-transitive closure of accessibility relations, and this closure is not first-order (and therefore, not coherently) definable. Something more must be done to capture the PDL family of logics.
In this paper we provide the first step towards a uniform proof theory of the sort that is currently missing for this family of logics by giving two new proof systems for PDL. We combine two ingredients from modern proof theory that have hitherto remained separate: labelled deduction à la Negri and non-wellfounded and cyclic sequent calculi.
We first construct a labelled sequent calculus , extending that of Negri [26], in which proofs are permitted to be infinitely tall. For this system soundness (via descending counter-models) and cut-free completeness (via counter-model construction) are proved in a similar manner to Brotherston and Simpson’s infinitary proof theory for first-order logic with inductive definitions [5]. Next we restrict attention to regular proofs, meaning only those infinite proof trees that are finitely representable (i.e. only have a finite number of distinct subtrees), obtaining the cyclic system . This can be done by permitting the forming of backlinks (or, cycles) in the proof tree, granted a (decidable) trace condition guaranteeing soundness can be established. We then show that the axiomatisation of PDL [21] can be derived in , obtaining completeness. We finish the paper with an investigation of proof-search in the cyclic system for a sub-class of sequents, and conjecture cut-free completeness for the test-free fragment of PDL.
Most crucially, this gives a simple (finitary) sequent calculus that elegantly handles iteration in a fashion reflecting actual reasoning about the operation. We conjecture that this system can be adapted to uniformly handle, not just additional program constructs that are found in the PDL literature, but also other modal logics (for example, epistemic logics with common knowledge modalities) whose interpretation requires the transitive closure of accessibility relations, which are perhaps also defined by coherent axioms. We discuss this, and a plan for future work in the conclusion.
For space reasons we elide proofs, but include them in an appendix.
Related Work.
Beyond the proof systems outlined above, the most significant related work can be found in Das and Pous’ [8, 9] cyclic proof systems for deciding Kleene algebra (in)equalities. Das and Pous’ insight that iteration can be handled in a cyclic sequent calculus is essential to our work here, although there are additional complexities involved in formulating a system for PDL because of the interaction between programs (which form a Kleene algebra with tests) and formulae. We also note that Goré and Widmann’s tableau procedure also utilises the formation of cycles in proof trees. Our proof of cut-free completeness of the infinitary system also follows that of Brotherston and Simpson [5] for first-order logic with inductive definitions.
Recent work by Cohen and Rowe [7] gives a cyclic proof system for the extension of first-order logic with a transitive closure operator and we conjecture that our labelled cyclic system (and labelled cyclic systems for modal logics more generally) can be formalised within it. This idea echoes van Benthem’s suggestion that the most natural setting for many modal logics is not first-order logic, but in fact first-order logic with a least fixed point operator [4].
Cyclic proof systems have also been defined for some modal logics with similar model properties to PDL, including the logic of common knowledge [38] and Gödel-Löb logic [35]. The idea of cyclic proof can be traced to modal -calculus [28]. Indeed, it can be shown that the logic of common knowledge [2], Gödel-Löb logic [4, 37] and PDL [4, 6] can be faithfully interpreted in the modal -calculus, indicating that perhaps cyclic proof was the right approach for PDL all along.
2 PDL: Syntax and Semantics
The syntax of PDL formulas is defined as follows. We assume countably many atomic propositions (ranged over by , , ), and countably many atomic programs (ranged over by , , ).
Definition 1 (Syntax of PDL)
The set of formulas (, , ) and the set of programs (, , ) are defined mutually by the following grammar:
[TABLE]
We briefly reprise the semantics of PDL (see [21, §5.2]). A PDL model is a Kripke model consisting of a set of states and an interpretation function that assigns: a subset of to each atomic proposition; and a binary relation on to each atomic program. We inductively construct an extension of the interpretation function, denoted , that operates on the full set of propositions and programs.
Definition 2 (Semantics of PDL)
Let be a PDL model. We define the extended interpretation function inductively as follows:
[TABLE]
where denotes relational composition, denotes the composition of with itself times, returns a set by projecting the first component of each tuple in a relation, and denotes the identity relation over the set .
We write to mean , and to mean that for all states . A PDL formula is valid when for all models .
3 An Infinitary, Labelled Sequent Calculus
We now define a sequent calculus for deriving theorems (i.e. valid formulas) of PDL. This proof system has two important features. The first is that it is a labelled proof system. Thus sequents contain assertions about the structure of the underlying Kripke models and formulas are labelled with atoms denoting specific states in which they should be interpreted. Secondly, we allow proofs of infinite height.
We assume a countable set of labels (ranged over by , , ) that we will use to denote particular states. A relational atom is an expression of the form , where and are labels and is an atomic program. A labelled formula is an expression of the form , where is a label and is a formula. We define a label substitution operation by when , and otherwise. We lift this to relational atoms and labelled formulas by: and .
Sequents are expressions of the form , where and are finite sets of relational atoms and labelled formulas. We denote an arbitrary member of such a set using , , etc. As usual, and both denote the set , and denotes the application of the (label) substitution to all the elements in . We denote by the set of formulas obtained from by prepending the modality to every labelled formula. That is, we define . denotes the set of all labels ocurring in the relational atoms and labelled formulas in .
We interpret sequents with respect to PDL models using label valuations , which are functions from labels to states. We write to mean that . We write to mean . For a sequent , denoted by , we write to mean that for some whenever for all . We write whenever this is not the case, i.e. when for all and for all . We say is valid, and write , when for all models and valuations that map each label to some state of .
The sequent calculus is defined by the inference rules in fig. 1. A pre-proof is a possibly infinite derivation tree built from these inference rules.
Definition 3 (Pre-proof)
A pre-proof is a possibly infinite (i.e. non-well-founded) derivation tree formed from inference rules. A path in a pre-proof is a possibly infinite sequence of sequents such that is the root sequent of the proof, and is a premise of for each .
Not all pre-proofs derive sound judgements.
Example 1
The following pre-proof derives an invalid sequent.
[TABLE]
Note that, since our sequents consist of sets of formulas, each instance of the (R) rule incorporates a contraction
To distinguish pre-proofs deriving valid sequents, we define the notion of a trace through a pre-proof. Traces consist of trace values, which (uniquely) identify particular modalities within labelled formulas. denotes a sequence , and denotes the empty sequence. We sometimes omit the subscript indicating length, writing , when irrelevant or evident from the context.
Definition 4 (Trace Value)
A trace value is a tuple consisting of a label , a (possibly empty) sequence of programs, a program , and a formula . We call the spine of , and the focus of . We write for the trace value , and for the trace value . In an abuse of notation we also use to denote the corresponding labelled formula .
Trace values in the conclusion of an inference rule are related to trace values in its premises as follows.
Definition 5 (Trace Pairs)
Let and be trace values, with sequents and (respectively denoted by and ) the conclusion and a premise, respectively, of an inference rule ; we say that is a trace pair for when and and the following conditions hold.
- (1)
If is the principal formula of the rule instance, then is its immediate ancestor and moreover if the rule is an instance of:
(R)
then , where is the label of the principal formula;
(R)
then ;
(;R)
then and for some trace value ;
(R)
then there is some such that: ; if is the left-hand premise; and if is the right-hand premise;
(R)
then if is the left-hand premise, and if is the right-hand premise. 2. (2)
If is not the principal formula of the rule then if the rule is an instance of (Subst) and is the label substituted, and otherwise.
If is the principal formula of the rule instance and the spine of is empty, then we say that the trace pair is progressing.
Notice that when a trace pair is progressing for , it is necessarily the case that the corresponding rule is an instance of (R) and that is the right-hand premise (although, not necessarily vice versa).
Traces along paths in a pre-proof consist of consecutive pairs of trace values for each corresponding step of the path.
Definition 6 (Trace)
A trace is a (possibly infinite) sequence of trace values. We say that a trace follows a path in a pre-proof when there exists some such that each consecutive pair of trace values is a trace pair for ; when , we say that the trace covers the path. We say that the trace progresses at if is progressing, and say the trace is infinitely progressing if it progresses at infinitely many points.
Proofs are pre-proofs that satisfy a well-formedness condition, called the global trace condition.
Definition 7 (Infinite Proof)
A proof is a pre-proof in which every infinite path is followed by some infinitely progressing trace.
Example 2
Figure 2 shows a finite representation of a proof of the formula . The full infinite proof can be obtain by unfolding the cycle an infinite number of times. An infinitely progressing trace following the (unique) infinite path in this proof is indicated by the underlined programs highlighted in blue, which denote the focus of the trace value in each sequent. The progression point is the (only) instance of the (R) rule.
Figure 3 shows a finite representation of a proof of the sequent . This proof is more complex than that of fig. 2, and involves two overlapping cycles. This proof contains more than one infinite path (in fact, it contains an infinite number of infinite paths). However, they fall into three categories:
(1) those that eventually traverse only the upper cycle;
(2) those that eventually traverse only the lower cycle; and
(3) those that traverse both cycles infinitely often.
Infinite paths of the first variety have an infinitely progressing trace indicated by the overlined programs highlighted in red. The progression point is the upper instance of (R) rule, marked by . The remaining infinite paths have a trace indicated by the underlined programs highlighted in blue. This trace does not progress around the upper cycle (for those paths that traverse it), but does progress once around each lower cycle at the instance of the (R) rule marked by . Since these paths traverse this lower cycle infinitely often, the trace is infinitely progressing.
Remark 1
The notion of trace in the system for Kleene Algebra of Das and Pous [8, 9] appears simpler than ours: a sequence of formulas (on the left) connected by ancestry, with such a trace being valid if it is principal for a (left) unfolding rule infinitely often. In fact, we can show that our definition of trace is equivalent to an analogous formulation of this notion for our system. However, our definition allows for a direct, semantic proof of soundness via infinite descent. In contrast, the soundness proof in [9] relies on cut-admissibility and an inductive proof-theoretic argument for the soundness of the cut-free fragment. It is unclear that a similar technique can be used to show soundness of the cut-free fragment of our system. Furthermore, the cut-free fragment of the system of Das and Pous is notable in that it admits a simpler trace condition than the full system: namely, that every infinite path is fair for the (left) unfolding rule [9, prop. 8]. Our system does not satisfy this property, due to the ability to perform contraction and weakening, as demonstrated in example 1.
The proof system is sound since, for invalid sequents, we can map traces to decreasing sets of counter-examples in (finite) models.
A path in a model is a sequence of states in such that each successive pair of states satisfies for some . A path in is called loop-free if it does not contain any repeated states. If and are paths in , we write to denote that is a prefix of .
An -partition of a path is a sequence of increasing indices . A path in for a trace value with respect to a valuation is a path in with having an -partition satisfying for each and , where we take (i.e. ). The -partition is called a partition of for . A counter-example in for a trace value at is simply a path in for w.r.t. such that .
A given path in for at can, in general, have many different partitions. A partition of a path for at is called maximal if the length of its final segment is maximal among all such partitions. We define the weight of a path in for at to be the length of the final segments of its maximal partition(s). We denote this by . If is a set of paths in for at , we define the measure of , denoted , to be the multiset of weights of the paths it contains; that is .
The measure for trace values in a model at a valuation , then, is simply the measure of the set of all of its ‘nearest’ counter-examples.
Definition 8 (Trace Value Measure)
Let denote the set of all loop-free counter-examples in for at such that there is no counter-example in for at with . The measure of in at is defined as .
For finitely branching models , it is clear that trace value measures are always finite. Note that finite multisets of elements of a well-ordering can be well-ordered using, e.g., the Dershowitz-Manna ordering [11]. This means that we have the following property.
Lemma 1 (Descending Counter-models)
Let , denoted , be the conclusion of an instance of an inference rule, and suppose there is a finitely branching model and valuation such that , then there is a premise of the rule instance, denoted , and a valuation such that and for each trace pair for , and also if is progressing.
This entails the soundness of our proof system, since PDL has the finite model property [12, Thm. 3.2]. This property states that, if a PDL formula is satisfiable, then it is satisfiable in a finite (and thus finitely branching) model. Thus, if a sequent is not valid then there is a finitely branching model that falsifies it. If a proof were to derive an invalid sequent, then by lemma 1 it would contain an infinite path for which there exists a finite model and a matching sequence of valuations that invalidate each sequent in the path. Moreover, these invalidating valuations ensure that the measures of the trace values in any trace pair along the path is decreasing, and strictly so for progressing trace pairs. However, since is a proof, it satisfies the global trace condition. This means that there would be an infinitely progressing trace following the path and thus we would be able to construct an infinitely descending chain of (finite) trace value measures. Because the set of finite trace value measures is well-founded, this is impossible and so the derived sequent must in fact be valid.
Theorem 3.1 (Soundness)
* derives only valid sequents.*
The cyclic system is obtained by restricting consideration to only those proofs of that are regular, i.e. have only a finite number of distinct subtrees.
Definition 9 (Cyclic Pre-proof)
A cyclic pre-proof is a pair consisting of a finite derivation tree possibly containing open leaves called buds, and a function assigning to each bud an internal node of the tree, called its companion, with a syntactically identical sequent.
We usually represent a cyclic pre-proof as the graph induced by identifying each bud with its companion (as in figs. 2 and 3). The infinite unfolding of a cyclic pre-proof is the pre-proof obtained as the limit of the operation that replaces each bud with a copy of the subderivation concluding with its companion an infinite number of times. A cyclic proof is a cyclic pre-proof whose infinite unfolding satisfies the global trace condition. As in other cyclic systems (e.g. [5, 7, 34, 36]) it is decidable whether or not this is the case via a construction involving complementation of Büchi automata. This means that decidability of the global trace condition for pre-proofs is PSPACE-complete.
Since every is also a proof, soundness of the cyclic system is an immediate corollary of theorem 3.1.
Corollary 1
If is derivable in , then is valid.
4 Completeness
In this section, we give completeness results for our systems. We show that the full system, , is cut-free complete. On the other hand, if we allow instances of the (Cut) rule, then every valid theorem of PDL has a proof in the cyclic subsystem .
4.1 Cut-free Completeness of
We use a standard technique of defining a pre-proof that encodes an exhaustive search for a cut-free proof (as used in, e.g., [5, 7]). For invalid sequents, this results in a pre-proof from which we can construct a counter-model, using the formulas that occur along a particular path.
A schedule is an enumeration of labelled non-atomic formulas in which each labelled formula occurs infinitely often. The th element of is written .
Definition 10 (Search Tree)
Given a sequent and a schedule , we can define an infinite sequence of open derivations inductively. Taking , we construct each from its predecessor by:
firstly closing any open leaves for which for some or by applying weakening rules leading to an instance of () or an axiom for some (thus the antecedent of each remaining open node is disjoint from its consequent); 2. 2.
then replacing each remaining open node in which occurs with applications of the rule for which is principal in the following way.
- •
If , then we pick a label not ocurring in , and replace the open node with the following derivation.
[TABLE]
- •
If then, letting be the set of all such that , we replace the open node with the following derivation.
[TABLE]
- •
In all other cases, we replace the open node with an application of the appropriate rule () as follows, where and , , are the sets of left and right immediate ancestors of , respectively, for the appropriate premise.
[TABLE]
Since each is a prefix of , there is a smallest derivation containing each as a prefix. We call this derivation a search tree for (w.r.t. ).
Notice that search trees do not contain instances of the (Cut) or (Subst) rules. Moreover, when a given search tree is not a valid proof, we may extract from it two sets of labelled formulas and relational atoms that we can use to construct a countermodel. If is not a valid proof, then either it contains an open node to which no schedule element applies or it contains an infinite path that does not satisfy the global trace condition (an untraceable branch). For a search tree , we say that a pair is a template induced by when either:
(i) is an open node of ; or
(ii) and , where is an untraceable branch in .
Notice that, due to the construction of search trees, the component sets of a template are necessarily disjoint. Given a template, we construct a PDL model as follows.
Definition 11 (Countermodel Construction)
Let be a template induced by a search tree. The PDL model determined by the template P is given by , where is the following interpretation function:
for each atomic proposition ; and 2. 2.
for each atomic program .
We write for the valuation defined by for each label .
PDL models determined by templates have the following property.
Lemma 2 ()
Let be a template induced by a search tree. Then we have for all and for all .
Lemma 2 entails the cut-free completeness of .
Theorem 4.1 (Completeness of )
If is valid, then it has a cut-free proof.
4.2 Completeness of for PDL
We show that the cyclic system can derive all theorems of PDL by demonstrating that it can derive each of the axiom schemas and inference rules in fig. 4, which (along with the axiom schemas of classical propositional logic) constitute a complete axiomatisation of PDL [21, §7.1].
The derivation of the axioms of classical propositional logic is standard, and eqs. 3 to 6 are immediately derivable via the left and right proof rules for their corresponding syntactic constructors. Each such derivation is finite, and thus trivially a proof. Equations 1, 2, 7 and Nec require the following lemma showing that a general form of necessitation is derivable.
Lemma 3 (Necessitation)
For any labelled formula , program , and finite set of labelled formulas such that , there exists a derivation concluding with the sequent and containing open leaves of the form such that:
- (i)
for each trace value , every path from the conclusion to an open leaf is covered by a trace ; and 2. (ii)
every infinite path is followed by an infinitely progressing trace.
Schemas for deriving eqs. 1, 2 and 7 are shown in fig. 5. Any infinite paths which exist in the schemas for deriving eqs. 1 and 2 are followed by infinitely progressing traces by lemma 3. Thus, they are proofs. In the schema for eq. 7, the open leaves of the subderivation constructed via lemma 3 are converted into buds, the companion of each of which is the conclusion of the instance of the (R) rule. Condition i of lemma 3 guarantees that each infinite path along these cycles has an infinitely progressing trace. We thus have the following completeness result.
Theorem 4.2 ()
If is valid then is derivable in .
It should be noted that theorem 4.2 is not a deductive completeness result, i.e. it does not say that any sequent is only valid if there is a proof for it. This is no major restriction, as a finitary syntactic consequence relation cannot capture semantic consequence in PDL: due to the presence of iteration, PDL is not compact. This can only be rectified by allowing infinite sequents in the proof system, which is undesirable for present purposes.
5 Proof Search for Test-free, Acyclic Sequents
In this section, we describe a cut-free proof-search procedure for sequents containing formulas without tests (i.e. programs of the form ), and for which the relational atoms in the antecedents do not entail cyclic models. We give a proof sketch that it is complete for this class of sequents.
Our approach relies on the following notion of normal form for sequents. For a set of relational atoms and labelled formulas, we write for the set . We call formulas of the form basic, those of the form iterated, and the remaining non-atomic formulas composite.
Definition 12 (Normal Sequents)
A sequent is called normal when:
(1) ;
(2) contains only labelled atomic and iterated formulas; and
(3) contains only relational atoms, labelled atomic formulas, and labelled basic formulas for which there is no such that also .
We say that reaches (or is reachable from ) in when there are labels and atomic programs such that and with for each . We say that a sequent is cyclic if there is some such that reaches itself in ; otherwise it is called acyclic.
Crucially, the following forms of weakening are validity-preserving.
Lemma 4 (Validity-preserving Weakenings)
The following hold.
- 4(1)
If is valid and , then is valid. 2. 4(2)
If normal is valid with , then is valid. 3. 4(3)
If normal is valid with , then is valid. 4. 4(4)
If normal is valid, for all , and not reachable in from any , then is valid.
An unwinding of a sequent is a possibly open derivation of obtained by applying axioms and left and right logical rules as much as possible, and satisfying the properties that: no trace progresses more than once; and all rule instances consume the active labelled formula of their conclusion, but preserve in the premise any relational atoms. A capped unwinding is an unwinding for which:
(a) weakening rules and (Ax) and () have been applied to all open leaves with or ; and
(b) the sequence of weakenings in lemma 4 have been exhaustively applied to all other open leaves.
Lemma 5 ()
*Let be a capped unwinding for (denoted ) and an open leaf (denoted ) of . The following hold:
(1) is normal;
(2) if is valid, then so are all the open leaves of ; and
(3) For every trace covering the path from to , if is a sub-formula of , then the trace is progressing.
We call a sequent test-free if it does not contain any programs of the form . A crucial property for termination of the proof-search is the following.
Lemma 6 ()
Let be a capped unwinding for a test-free, acyclic sequent; then is finite, and for all open leaves of .
Both cyclicity and the presence of tests can cause lemma 6 to fail, since then it is possible for there to be a path of ancestry between two occurrences of an antecedent formula that traverses an instance of the (L) rule. That is, antecedent formulas may be infinitely unfolded. Moreover, in the presence of tests or cyclicity, the weakenings of lemma 4(4) do not result in for open leaves .
We define a function on test-free sequents (details are given in the appendix), whose purpose is to provide a bound ensuring termination of proof-search. Although, at time of submission, we do not have a fully detailed proof, we believe that it satisfies the following property for capped unwindings of test-free, acyclic sequents : \left|\{x:\varphi\in\Delta^{\prime}\mid\text{\varphi non-atomic}\}\right|\leq\operatorname{\ast\text{-}\mathsf{max}}({\Gamma}\Rightarrow{\Delta}) and for all open leaves of .
Proof-search proceeds by iteratively building capped unwindings for open leaves. All formulas encountered in the search are in the (finite) Fischer-Ladner closure of the initial sequent, and validity and acyclicity are preserved throughout the procedure. Lemma 6 and the above property will ensure that the number of distinct open leaves (modulo relabelling) encountered during proof-search is bounded, so we may apply substitutions to form back-links during proof-search. Lemma 5(3) ensures that the resulting pre-proof satisfies the global trace condition. For invalid sequents, proof-search produces atomic sequents that are not axioms. We thus conjecture cut-free regular completeness for test-free PDL.
Conjecture 1 ()
If test-free is valid, has a cut-free proof.
6 Conclusion
In this paper we have given two new non-wellfounded proof systems for PDL. allows proof trees to be infinitely tall, and restricts to the proofs of that are finitely representable as cyclic graphs satisfying a trace condition. Soundness and completeness of both systems was shown, in particular, cut-free completeness of and a strategy for cut-free completeness of for test-free PDL.
There is much further work to be done. Of immediate interest is the verification of cut-free regular completeness for test-free PDL, and the extension of the argument to the full logic. We would also like to consider additional program constructs. Some, like converse, can already be treated through De Giacomo’s [15] efficient translation of Converse PDL into PDL. It may be more desirable, however, to represent the program construct directly, to aid in the modular combination of different constructs. One construct that is particularly notorious is Intersection. Despite the modal definability of its dual, Choice, the intended interpretation of Intersection is not modally definable, and the completeness (and existence) of an axiomatisation for it remained open until Balbiani and Vakarelov [3]. An earlier, and significantly simpler, solution to this problem was the augmentation of PDL with nominals, denoted Combinatory DL [30]. We conjecture that the presence of labels in our system enables us to perform a similar trick, without contaminating the syntax of the logic itself. However we should note that a key prerequisite of our soundness proof, namely the finite model property of PDL, no longer applies to PDL with intersection. We therefore have the non-trivial task ahead of us of weakening this assumption.
Our work should be seen as a part of a wider program of research to give a uniform and modular proof theory for a larger group of modal logics, including what we have denoted PDL-type logics. One source of modularity and uniformity is the existing Negri labelled system our calculi extend. This allows us to freely add proof rules corresponding to first-order frame axioms defining Kripke models. A wider class of modal logics than those directly covered by Negri’s framework are those with accessibility relations that are defined to be wellfounded or arise as transitive closures of other accessibility relations (we note Negri is able to treat the specific case of Gödel-Löb logic due to its special interpretation of , but not the general class we describe). We believe an appropriate framework to uniformly capture these logics as well is cyclic labelled deduction. We are encouraged in this pursuit by recent work of Cohen and Rowe [7] in which first-order logic with a transitive closure operator is given a cyclic proof theory. We may think of labelled deduction as a way of giving a proof theoretic analysis of the first-order theory of Kripke models and their modal satisfaction relations. Labelled cyclic deduction, we conjecture, can be seen as the first-order-with-least-fixpoint theory of Kripke models and satisfaction relations.
Finally, and somewhat more speculatively, with the cyclic system in hand we intend to investigate the hitherto open problem of interpolation for PDL. This has seen no satisfactory resolution in the years since PDL was first formulated, with the only attempted proofs strongly disputed [25] or withdrawn [24]. It would be interesting to see if the existence of a straightforward proof system for the logic opens up any new lines of attack on the problem. For example, Lyndon interpolation has been proved for Gödel-Löb logic using a cyclic system [35].
Appendix: Proofs
Soundness
Before proving lemma 1, we recall the following property of (cf. [23, §8(C)]), where we write for the multiplicity of in the multiset .
Property 1
For finite multisets and consisting of elements of a partial order , if and only if:
- •
; and
- •
for all , if then there is such that and .
We therefore have the following properties. We call a function from a set of paths in for at to another set of paths in for at size-increasing when it satisfies for all , and strictly size-increasing when for at least one .
Proposition 1
Let and be non-empty finite sets of paths in for and at and , respectively, and let be injective. Then the following hold.
- 1(2).
If is strictly size-increasing then . 2. 1(2).
If is size-increasing then .
Proof
- (1)
Notice that since is finite there is some maximal such that there is some path with (i.e. a greatest path weight in that is strictly increased by ). Therefore there is some such that —simply take for some such that —and so . Moreover, notice that for all . Thus, if we have such that it must be that . But then the second condition of property 1 is satisfied since we have and . Thus . 2. (2)
We distinguish two cases.
- •
If, in fact, for all then we distinguish two further sub-cases. On the one hand, if is surjective then we have that , and therefore immediately . On the other hand, when is not surjective then we have (since contains more paths) but , for all ; thus the second condition of property 1 is trivially satisfied and so in fact . Therefore also .
- •
If there is some such that , then is in fact strictly size-increasing. Thus we have from the previous result that , and so also . ∎
We now prove the descending counter-models lemma.
See 1
Proof
Let be the conclusion of an instance of an inference rule; suppose is a finitely branching model and such that . We do a case analysis on the inference rule. Recall that: trace value measures are always finite for finitely branching models; and the set of counter-examples for any trace value in an invalid sequent is necessarily non-empty.
(Ax), ():
The result holds vacuously since it is clear that these rules derive valid sequents.
(Subst):
Straightforward. We take . For any trace pair , the sets of counter-examples in for and at and , respectively, are equal. Thus we have and so trivially .
(Classical connectives, left modal rules, Cut):
These cases are straightforward: taking suffices. Moreover, in these cases each trace pair is such that (and therefore non-progressing); thus the trace condition holds straightforwardly because then the sets of counter-examples in for and at and , respectively, are equal. Thus we have and so trivially .
(R):
Then is and is of the form for some fresh . Since we have that there is some state in such that and . So we take , for which we have . For all (non-progressing) trace pairs in the context , we have with label , and so . Thus and therefore trivially . For trace pairs where and , we reason as follows. Notice that we have only if . That is, defined by is an injection from to . Notice also that if is a partition for then is a partition for . Therefore, . To see this, take some maximal weight partition of , with weight ; then we know that is a partition for . The weight of is clearly also , and so the weight of the maximal partition of for at must be at least . In summary, is size-increasing. So, by item 1(2), .
(;R):
Then is and is . We take since, if is a state in such that and , then by definition 2 there is some state in with and . For all (non-progressing) trace pairs in the context , we have ; so and therefore holds trivially. For (non-progressing) trace pairs where and for some we reason as follows. Notice that we have (if and) only if . Moreover, if is a partition for then is a partition for . Therefore, . To see this, take some maximal weight partition of , with weight ; then we know that is a partition for . The weight of is clearly also , and so the weight of the maximal partition of for at must be at least . In summary, the identity function is a size-increasing injection from to . So, by item 1(2), .
(R):
Then is . We take . If is a state in such that and then, by definition 2, either or . If the former we take the left-hand premise for , and if the latter then we take the right-hand premise. In both cases, notice that we can reason as follows. Firstly, since , for all (non-progressing) trace pairs in the context , we have ; so and therefore trivially . Secondly, for (non-progressing) trace pairs where , and (with or ) for some , we reason as follows. Notice that we have only if . Moreover, if is a partition for then is also a partition for . Therefore, . To see this, take some maximal weight partition of , with weight ; then we know that is also a partition for . Thus the weight of the maximal partition of for at must be at least . In summary, the identity function is a size-increasing injection from to . So, by item 1(2), .
(R):
Then is and is . We take since, if is a state in with such that then, by definition 2, and . Thus, for all (non-progressing) trace pairs in the context , we have ; so and therefore trivially . For (non-progressing) trace pairs , we have , and we can reason as follows. Notice that we have (if and) only if . Moreover, if is a partition for then is a partition for . Therefore, . To see this, take some maximal weight partition of , with weight ; then we know that is also a partition for . The weight of is clearly also , and so the weight of the maximal partition of for at must be at least . In summary, the identity function is a size-increasing injection from to . So, by item 1(2), .
(R):
Then is . We take . Since , there is a state in with such that . Then, there are two possibilities. If then we take the left-hand premise and so is . On the other hand, if in fact then and we have that for some . Therefore there is a state in with and . In this case, the right-hand premise is invalidated and so we take is . In both cases, for the (non-progressing) pairs in the context we have ; so and so trivially . For the remaining trace pairs, there are two cases.
- •
If is the left-hand premise, then we reason as follows. In this case . Notice that only if . Moreover, if is a partition for then is a partition for . Therefore, . To see this, take some maximal weight partition of , with weight ; then we know that is also a partition for . The weight of is clearly also , and so the weight of the maximal partition of for at must be at least . In summary, the identity function is a size-increasing injection from to . So, by item 1(2), .
- •
If is the right-hand premise, then recall we have and so for all . Here we have , with progressing if and only if the spine of is empty. Notice that, for this case, we have (if and) only if . Moreover, if is a partition for then is a partition for . Therefore, . To see this, take some maximal weight partition of , with weight ; then we know that is also a partition for . The weight of is clearly also , and so the weight of the maximal partition of for at must be at least . In summary, the identity function is a size-increasing injection from to . So, by item 1(2), . Now, as noted above for all , and so for any partition of we have that and so . Thus, in the case that the spine of is empty, we have . That is, for the progressing trace pair, the identity function is a strictly size-increasing injection from to and so, by item 1(2), . ∎
See 3.1
Proof
Take a proof of a sequent and assume for contradiction that it is not valid. Since PDL has the finite model property, there is a finitely branching model and that falsifies it. Then, by lemma 1, must contain an infinite path for which there exists a sequence of valuations that invalidate each sequent in the path. Moreover, these invalidating valuations give rise to measures for the trace values that ensure the measure of any trace pair along the path is decreasing, and strictly so for progressing trace pairs. However, since is a proof, it satisfies the global trace condition. Thus there is an infinitely progressing trace along the path and therefore we can construct an infinitely descending chain of (finite) trace value measures. But this contradicts the fact that the set of finite trace value measures is well-founded. So conclude that must in fact be valid. ∎
Completeness
See 2
Proof
By induction on the structure of formulas.
():
The first conjunct follows trivially since, by construction of the search tree, cannot be in . If then the result follows immediately since by definition 2.
(relational atom, or atomic formula ):
Immediate by definition 11, since and are disjoint.
(, , ):
Straightforward induction.
():
The first conjunct is entailed by the following property, which we show for all programs , labels and , and formulas .
[TABLE]
To see this, assume that . We need to show that for all such that . But this follows immediately by induction, since we have from eq. A that (note that the subprogram relation is reflexive). We prove eq. A by an inner induction on the structure of programs.
- •
For an atomic program , assume and . From the latter, by definition 11, it must be that . Thus, the result follows from the construction of the search tree (cf. definition 10).
- •
Composition and choice follow by a straightforward induction.
- •
For a test , notice that since is a subprogram of we have that the outer induction applies to . Assume that . Thus by definition 2, we have and . Assume also that . By construction of the search tree, either or . The result obtains since the latter cannot hold; else by the outer induction we have that , i.e. .
- •
For iteration, assume . So, there are labels with and such that for each . Now assume that . It suffices to show that if there are labels with for each and , then both and . This follows by a further induction on . For , the result follows immediately by construction of the search tree. For , by the induction on . Then by the induction on eq. A we have that , whence the result follows again by construction of the search tree.
The second conjunct is entailed by the following property, which we again show for all programs , labels , and formulas . Let be the untraceable branch from which the template is derived.
[TABLE]
To see this, assume ; thus for some . We need to show that for some such that . But this follows immediately by induction, since we have from eq. B that for some and , and thus by definition, with . Again, we prove eq. B by an inner induction on the structure of programs. The clause relating to traces is needed for iteration.
- •
For an atomic program , assume . By construction of the search tree, and for some , and there is a trace covering the path for every trace value . Thus, the result follows since then by definition 11.
- •
Composition and choice follow by a straightforward induction.
- •
For a test , notice that since is a subprogram of we have that the outer induction applies to . Assume that . By construction of the search tree, we have that both and for some , and there is a trace covering the path for every trace value . Thus, by the outer induction . So by definition 2, whence the result follows taking .
- •
For iteration, assume . By the construction of the search tree and the inner induction, we have for some :
(i) either and there is a trace covering the path for every trace value ; or
(ii) for some with and there is a trace covering the path for every trace value , which is progressing for , where is the empty sequence.
Therefore, there must be some and with such that , for each , and for every trace value there is a trace covering the path . If not there would be an infinitely progressing trace covering the untraceable branch, which is impossible by definition. Thence the result follows, since by definition 2. ∎
Remark 2
It is only the presence of tests in programs that requires eqs. A and B above to be proved via a nested induction. Without tests, these properties may be proved independently.
See 4.1
Proof
Suppose is valid. Let be a search tree for . It must be that is a (cut-free) proof. Supposing otherwise, it would induce some template . Since, by construction, and , it then follows from lemma 2 that the model determined by satisfies all and falsifies all (i.e. is a countermodel); thus is not valid. However, this contradicts our initial supposition that is valid and so must indeed be a proof. ∎
See 3
Proof
By induction on . In the following, a double rule indicates zero or more applications of the indicated rule(s).
(atomic ):
We pick a fresh label and construct the following derivation.
[TABLE]
In the case that is empty, we apply an instance of the (WL) rule rather than (L). Note here that there is a single open leaf, and no infinite paths in the derivation. It is clear that, for any trace value , we can form a trace covering the path from the conclusion to the open leaf.
(composition ):
We construct the following derivation.
[TABLE]
For a trace value , take any path the from the conclusion to an open leaf and let and be the traces covering the portions of the path through the subderivations obtained from the induction. We can then form the trace covering the the full path. Any infinite paths in the derivation must be contained in one of the subderivations obtained from the induction, thus we also obtain the required infinitely progressing trace.
(choice ):
We construct the following derivation.
[TABLE]
For a trace value , take any path the from the conclusion to an open leaf and let be the trace covering the portion of the path through the subderivation obtained from the induction. We can then form the trace , if the path traverses the left–hand premise of the instance of the (R) rule, and otherwise. Note that this is the only case to cause the resulting derivation to have more than one open leaf. Again, any infinite paths in the derivation must be contained in one of the subderivations obtained from the induction, thus we also obtain the required infinitely progressing trace.
(test ):
Without loss of generality, suppose . Then define sets by . We construct a series of open derivations inductively as follows.
[TABLE]
[TABLE]
The required derivation is the following.
[TABLE]
If is empty, then we may just apply the (WL) rule instead of using derivation . Notice that there is a single open leaf in this derivation and, thus a single path from the conclusion to this leaf that traverses the right-hand premise of each instance of the (L) rule. For a trace value , w can construct the trace that covers this path. Notice also that there are no infinite paths in this derivation.
(iteration ):
We construct the following derivation.
[TABLE]
Here, we have converted each open leaf in the subderivation obtained via the inductive hypothesis into buds, with associated companion the sequent concluding the full derivation. This derivation thus has a single open leaf, above the left-hand premise of the instance of the (R) rule. The inductive hypothesis guarantees that every path from the conclusion of the subderivation to a bud is covered by a trace for each trace value . Thus, for each such trace value, there is a trace covering each cycle from the conclusion of the derivation back to itself. Now, any path from the conclusion to the open leaf must traverse a (finite) sequence of such cycles, before then traversing the left-hand premise of the instance of the (R) rule marked by and continuing to the leaf. We can thus concatenate the traces covering each basic cycle, and preprend this to the trace covering the final portion of the path from the conclusion to the open leaf. This shows that condition i holds.
To see that condition ii holds, notice that the infinite paths in this derivation fall into two categories: either the path remains within the subderivation obtained via the induction; or the path visits the conclusion of the derivation infinitely often. In the former case, we obtain by the induction that the path is followed by an infinitely progressing trace. In the latter, it must consist of an infinite sequence of cycles from the conclusion. Each such cycle is covered by a trace, as indicated by the underlined programs highlighted in blue, which progresses at the instance of the () rule marked with . Thus we have an infinitely progressing trace by concatenating these individual traces. ∎
See 4.2
Proof
If then there is a Hilbert deduction where . From such a deduction, we define a sequence of proofs inductively as follows. For each , if it is an instance of an axiom, then is the corresponding derivation of . If is derived from () via (Nec), then is the derivation constructed by applying lemma 3 for the sequent and replacing each open leaf with a copy of . If is derived from and () via (MP), then is the following derivation.
[TABLE]
Thus, is a proof of . ∎
Proof Search in for Test-free, Acyclic Sequents
See 4
Proof
If is valid then it has a cut-free (and substitution-free) proof , by theorem 4.1. Since , we must also have for any sequent in the proof. This follows from the fact that if is in the consequent but not the antecedent of the conclusion of a logical inference rule, then this property also holds of its premises. This is immediate for all rules except (R), which do not introduce new relational atoms in the premises and preserve their contexts. For (R), notice that although it may introduce a relational atom in the premise we must have since appears in the conclusion and must be fresh. Note that although weakening rules may be used to remove from the consequent, these are only used in the proof to lead to an axiom and so cannot occur in the antecedent of any sequent above such a weakening rule. The relational atom is thus never principal for any rule in , and so we can produce a proof of by removing from every consequent in in which it appears. Then, by theorem 3.1, is valid. 2. 2.
Since is valid it must have a cut-free proof , by theorem 4.1. We show that every sequent in satisfies:
(i) ;
(ii) and does not reach in for all with non-atomic;
(iii) for all with composite or iterated;
(iv) if then there is no non-atomic such that ; and
(v) if with non-atomic then does not reach in .
Note that the root sequent satisfies these since it is normal and . Furthermore, the proof rules used in preserve these properties from conclusion to premise. We take each invariant in turn.
(2i):
For rules (L), (L), (L) and (L), this follows from the fact that the conclusion satisfies item 3ii. For rule (R) and (R), this follows from the fact that the conclusion satisfies item 2ii. The result is straightforward or immediate for the other rules.
(2ii):
For (R), it is immediate since is fresh. For rules (L) and (L), this follows from the fact that the conclusion satisfies item 2iii. The result is straightforward or immediate for the other rules.
(2iii):
For rules (R) and (R), this follows from the fact that the conclusion satisfies item 2ii. For rule (R), this follows from the fact that the conclusion satisfies item 2iv. The result is straightforward or immediate for the other rules.
(2iv):
For rules (R) and (R), this is immediate since from the fact that the conclusion satisfies item 3ii we have for the principal formula . For rule (L), we must have that for the principal formula ; but then because the conclusion satisfies item 2v we have that does not reach in and so . For (R), we have that for the principal formula since the conclusion satisfies item 3ii; so the result follows trivially since we the new relational atom in the premise does not involve . The result is straightforward or immediate for the other rules.
(2v):
For rule (L), the result is immediate since in the premise is fresh. For rule (R), we have for the principal formula since the conclusion satisfies item 3iii, and by assumption that does not reach in ; but then does not reach in , otherwise then so would . For rules () and (R), the result is immediate since the conclusion satisfies item 2ii. For the remaining right-hand rules the result is immediate since they do not introduce new labelled formulas in the antecedents of the premises. For the remaining left-hand rules, it is also straightfoward since there is with non-atomic in the antecedent of a premise only if there is some with non-atomic in the antecedent of the conclusion.
Therefore, the formula is never principal for any rule in , and so we can produce a proof of by removing from every consequent in in which it appears. Then, by theorem 3.1, is valid. 3. 3.
Since is valid it must have a cut-free proof , by theorem 4.1. We show that every sequent in satisfies:
(i) ;
(ii) for all with composite or iterated; and
(iii) for any program and label , it holds that .
The root sequent satisfies these since it is normal (in particular, contains no labelled composite or iterated formulas), and . Furthermore, the proof rules used in preserve these properties from conclusion to premise. The non-trivial cases are the rules for atomic modalities and implications. In (L), since there is no relational atom in the antecedent of the conclusion, the active formula must satisfy , and so item 3ii is maintained in the premise. In (R), since is not in the labels of the consequent of the conclusion, the new relational atom in the premise preserves item 3iii; and because the new label in the premise is fresh, item 3i is also maintained. In (L), since the active formula in the conclusion satisfies , the new formula in the consequent of the left-hand premise maintains item 3i. Similarly for (L). In (R) and (R), since does not occur in the labels of the consequent of the conclusion, the new formula in the antecedent of the premise maintains item 3ii. Thus, the formula is never for any rule in , and so we can produce a proof of by removing from every antecedent in in which it appears. Then, by theorem 3.1, is valid. 4. 4.
Since is valid, by the construction for theorem 4.1 it must have a cut-free proof such that every sequent in (apart from the root) that is not the premise of a weakening rule contains its conclusion (i.e. its antecedent is a superset of the antecedent of its conclusion, and similarly for its consequent). It is straightforward to see that, for every rule, when the conclusion satisfies the property that or implies either or there is some that reaches in , then so does the premise. The only non-trivial cases are the atomic modality rules. For (R) rule, we have from the assumption on the conclusion that either or there is that reaches in for the principal formula . Therefore, because the relational atom is introduced in the premise, we have that or reaches in the premise antecedent. The (L) rule is, in fact, unproblematic since we have that each rule in preserves the active formula(s) of the conclusion in the context of the premises; thus, the reachability relation induced by the antecedents only grows from conclusion to premise. Thus, every sequent in satisfies this property, whence the we derive that the property holds for the premise. Now, it follows that the relational atom can never be active in ; if it were, there would be some sequent such that some corresponding labelled formula is in . But then we would have that either or is reachable from some label in , which contradicts the assumption that nor reachable from any label in . Therefore we can produce a proof of by removing from every antecedent in in which it appears. Then, by theorem 3.1, is valid. ∎
See 5
Proof
otherwise it would be closed by weakening and an instance of (Ax). can only contain labelled atomic and iterated formulas that have already been unfolded along the path from the root of the unwinding, otherwise the construction of the unwinding would be able to apply further logical rules. The third condition of definition 12 must hold similarly: otherwise the unwinding construction could apply further logical rules to . Moreover, the weakening steps of lemma 4 preserve these properties, since they only remove elements from sequents, and remove all relational atoms from the consequent. 2. 2.
In uncapped unwindings only logical rules are applied. Notice that these are invertible. Lemma 4 shows that the sequence of weakening rules applied to the open leaves of unwindings preserve validity. 3. 3.
Notice that all rules except (L) and (R) have the sub-formula property. Thus, if an ancestor formula contains its descendant as a sub-formula then the path of ancestry must be principal for one of these unfolding rules, whence we derive the result. ∎
To prove lemma 6, we need the following three results. Proposition 2 entails that the proof-search procedure preserves acyclicity. We use proposition 3 to show that in unwindings we cannot keep unfolding iterated formulas on the left forever. Proposition 4 gives that unwindings produce consequent formulas with terminal labels, which we use to show that open leaves of capped unwindings do not contain relational atoms.
Proposition 2
Let be a finite derivation consisting only of logical rules concluding with an acyclic sequent; then every sequent appearing in is acyclic.
Proof
By induction on the structure of derivations. The only non-trivial cases are the rules for atomic modalities. For (L), assume the conclusion is acyclic. Then the premise must be acyclic since its set of antecedent relational atoms is a subset of those of the conclusion. Then the result follows by induction. For (R), assume the conclusion is acyclic. Then the premise is acyclic since the new relational atom does not link to any existing label, being fresh. Then the result follows by induction.
Proposition 3
Let be a finite derivation consisting only of left logical rules and concluding with a test-free sequent ; then if it contains a path of ancestry from some ancestor antecedent formula to a descendent antecedent formula , with a sub-formula of , then reaches in .
Proof
By straightforward induction on the structure of derivations.
Proposition 4
Let be a possibly open finite derivation consisting only of logical rules that preserve relational atoms from conclusion to premise, and let be an open leaf of ; if there is a path of ancestry from that is principal for an instance of (R), then does not reach any label in .
Proof
By induction on the structure of derivations. Most cases are straightforward. The only interesting cases are those for the atomic modalities. For (L), assume the result holds for the premise; then it must continue to hold for the conclusion because the principal relational atom must already be in the antecedent of the premise, since the derivation only uses rules that preserve relational atoms from conclusion to premise. Thus, we do not increase reachability. For (R), the result holds by induction for formulas in the context, and if there is a path of ancestry already principal for an instance of (R) from to the principal formula in the premise. However here we need to further consider the following. Assume that there is a path of ancestry from to the principal formula in the premise with a sub-formula of , but not principal for an instance of (R). Thus, we must have . The immediate descendant of this formula, , is now connected by a path of ancestry that is principal for (R) to . So we must show that does not reach any label in . Note that must be fresh for the contexts and of the conclusion. Now, suppose reaches some label in ; then there must be some relational atom introduced into the left-hand context along the path up to the open leaf . But since the path of ancestry leading to is never principal for (R), this can only happen if there is an instance of (R) along the path that is principal for some other formula . However if this were the case then it would have a descendant in that is distinct from . This would contradict the side-condition of the rule: that is fresh, so we conclude that does not reach any label in after all.
We now give the proof of lemma 6.
See 6
Proof
For finiteness, it suffices to show that uncapped unwindings for test-free, acyclic sequents are finite, since no logical rules are applied during the capping process and the weakening rules strictly reduce the size of the sequent they are applied to. Suppose, for contradiction, that the unwinding is infinite. Then there must be an infinite path in the derivation containing either an infinite number of right-hand rules or an infinite number of left-hand rules. If it is the former then, since each rule in the derivation has the sub-formula property and each formula that appears is in the (finite) Fischer-Ladner closure of , there must be a consequent formula that is principal for (R) an infinite number of times. However, this is impossible since each consequent formula in an unwinding can only be unfolded at most once. So we may assume there are only a finite number of right-hand rules. If, then, there are an infinite number of left-hand rules, we must similarly have that there is a path of ancestry in which some antecedent formula appears an infinite number of times. Since there are only a finite number of right-hand rules, there is an infinite sub-derivation consisting only of left logical rules, and concluding with some sequent . Now, take a (necessarily finite) prefix of such that there are occurrences of the (L) rule for which the path of ancestry is principal, being the number of distinct labels in . By proposition 3, we must have that there are labels such that reaches each in (), where is on the path of ancestry. Therefore, we must have for some and with . That is, is cyclic. However this is also impossible by proposition 2, since we have assumed that is acyclic. Thus, we conclude must be finite after all.
The second part, that for open leaves , is ensured by the weakening rules that are applied to the open leaves of uncapped unwindings. To see that this is the case, note the following. The second category of weakening rules ensure that . The third category of weakening rules ensure that only if . The fourth category of weakening rules ensures there are no relational atoms in . The weakening steps remove relational atoms of the form such that and is not reachable in the antecedent of the open leaf of the unwinding from any label in . So we are left to account for relational atoms such that or is reachable from some label in . However, no such relational atoms exist. To see that this is the case, notice that the construction of the unwinding ensures that each with iterated has been unfolded once within the unwinding and so, because is test-free, this means that there is a path of ancestry from that is principal for a (R) rule. Then we have from proposition 4 that any such does not reach any label in . Now consider the two cases. If , then reaches since is in the open leaf of the unwinding; but this is impossible as we have shown that does not reach any label. The other case is also impossible from our previous reasoning that is not reachable from any label in .
We now define the functions that provide a bound on the possible number of distinct sequents (up to label substitution) encountered during proof search for test-free, acyclic sequents. These functions are defined for test-free formulas only. Addition and multiplication on natural numbers are denoted and , respectively. We use to denote the function on natural numbers. The set of words in the language of (a regular expression) with length at most is denoted by .
Definition 13 ()
We define the functions and by mutual induction as follows.
[TABLE]
The function on programs is defined as follows.
[TABLE]
We then define the function on pairs of labels and sequents, as follows.
[TABLE]
Intuitively, measures the maximum length of a path of reachability from the label that will be generated, by instance of the (R) rule, in an unwinding of the sequent . The auxiliary function gives the maximum length of a single ‘unfolding’ of the program .
The function is used for antecedent formulas, and for consequent formulas. For example, the case for conjunctions and disjunctions take the maximum of the values of each conjunct/disjunct because the proof rules split the formula. The maximum path length will the maximum of the maximum lengths for each of the constituent immediate sub-formulas. The rules for an implication switch the polarity for the antecedent sub-formula because the proof rules move this sub-formula to the opposite side.
The case for iteration differs for the two polarities. Modalities on the left do not contribute to reachability paths: the (L) is only activated by relational atoms, it does not generate them during proof-search. Thus, the case for modalities in simply recurses on the immediate sub-formula. Modalities on the right-hand side do contribute to reachability. The (R) rule has two premises: one simply strips off the modality, whereas the other one unfolds it. Therefore, the maximum path of reachability generated by an iterated formula is the maximum of that of its immediate sub-formula, on the one hand, and the maximum length of one copy of the iterated program , on the other. This is because an unwinding will unfold an iterated formula exactly once.
The function gives the maximum length of one copy of a program . Atomic programs have unit length; a composition has the sum of the lengths of the sub-programs, while with choice we take the maximum. As mentioned, iterations are unfolded exactly one, so for , simply recurses on the sub-program .
The maximum length of the path of reachability generated by an unwinding from a label in the initial sequent is then simply the maximum of those of the formulas that appear in labelled with .
We now define the function , which, intuitively, gives an upper bound on the number of number of labelled iterated formulas that will appear in the consequent (right-hand side) of the sequent in the open leaves of an unwinding of .
Definition 14 ()
We define the functions and , which operate on pairs of natural numbers and (test-free) formulas, by mutual induction as follows.
[TABLE]
The function , parameterised by test-free programs , takes words (sequences of atomic programs) to sets of indices, and is defined as follows.
[TABLE]
We then define the function on sequents, as follows.
[TABLE]
Here again, we define two functions with different ‘polarities’. For an initial sequent , gives the maximum number of consequent iterated formulas that will be generated along any path in an unwinding by an occurrence of in , provided it can make use of a reachability path of length at most . Similarly, gives the maximum number of consequent iterated formulas generated by . The reason we need a bound on the length of the available reachability path is precisely to reason about unfolding of antecedent iterated formulas. Indeed, the only case in which this parameter is used in the definitions above is in that for an antecedent modal formula, . Since the construction of an unwinding does not a priori bound the number of times such a formula can be unfolded. What actually prevents this process continuing ad infinitum is the fact that the path of reachability, which is generated by unfolding consequent iterated formulas and decomposing the resulting program modalities, is bounded by the fact that unfolding of consequent formulas can happen at most once. This principle can be seen at work in the proof of lemma 6.
The cases of the definition for conjunction, disjunction and implication should be relatively self-explanatory. For example, because the (R) rule decomposes a conjunction into two separate branches, takes the maximum of the values for the immediate sub-formulas. For a disjunction, it adds the values because the (R) rule decomposes the disjunction within the same branch. Similarly for an implication , the values are added as there is only a single premise for the (R) rule; notice the polarity switch for the recursion on the antecedent sub-formula . The defintion of for these cases is dual, since the left-hand proof rules are dual to the right-hand ones.
The most interesting cases of the definition are the ones for modalities. We first describe the case for consequent modal formulas . If is -free, then the modality will simply be decomposed, and so the function simply recurses on the immediate sub-formula . If contains iterations, then the modality will be decomposed until an iteration is reached; however note that the decomposition will lead to only one iteration in each branch. The (R) rule will then be applied; it has two premises. In the left-hand branch, the iteration is simply discarded, leaving the sub-formula . In the right-hand branch, the iteration is unfolded and this process will begin again. This eventually ends since iterated formulas will be unfolded exactly once, but we have that each path ends either with an iterated formula already unfolded or . Thus, the number of iterated formulas generated along any of these paths is the maximum of (for the former case), or that of (in the latter).
For antecedent modal formulas , the case is slightly more complex. These will be decomposed in potentially many ways according to the available paths of reachability, and so may lead to many occurrences of the sub-formula along the same branch. The definition of the case thus makes use of the information about the maximum length of these available paths of reachability. Any sequence of atomic programs (i.e. word) that is included in (i.e. is a model of) the program (i.e. regular expression) , and which has length at most can lead to a new occurrence of in the antecedent. Therefore we sum over all such words. The function gives the set of all iteration ‘boundaries’ for the sequence of atomic programs with respect to the program . That is, it gives the set of all indices such that an antecedent iterated formula can be unfolded to (essentially) , for some program , and thus decomposed to (provided there is a path of reachability from to via ). This means that the (L) rule will generate an antecedent formula . Therefore, takes the sum of for all iteration boundaries in all words of length up to that are in the language of the program . Since does not contain the index itself, also includes in the sum for all such words .
To compute the value of for a sequent, first the maximum length of the available reachability path for each label in the sequent is determined, using the function. Then, using this information, we take the sum of the value of (with the appropriate polarity) for each of the lablled formulas it contains.
For termination of proof-search, we need two properties. The first is that the number of consequent iterated formulas in the open leaves of unwindings is bounded as a function of the initial sequent, namely . The second is that the value of does not increase during proof-search. This means that the value of for the initial sequent of the proof-search gives a bound on the size of the conclusions of all unwindings constructed during the search. Thus, proof-search must terminate.
Proposition 5
For be a capped unwinding for test-free, acyclic , then \left|\{x:\varphi\in\Delta^{\prime}\mid\text{\varphi non-atomic}\}\right|\leq\operatorname{\ast\text{-}\mathsf{max}}({\Gamma}\Rightarrow{\Delta}) for all its open leaves .
The second property requires some auxiliary monotonicity results.
Lemma 7 (Path Monotonicity)
. 2. 2.
. 3. 3.
* for and .*
Proof
The first two are straightforward. If is a relational atom, the result is immediate since these do not contribute to the value of for sequents. If is a labelled formula , then there are two cases to consider. For the case the result is immediate since the set of formulas from which we take the maximum does not change. If on the other hand , the result is straightforward since we only add a formula to the set from which we take the maximum: if (resp. ) is less than (resp. ) for some (resp. ), then the value of for the two sequents are the same; otherwise it is greater for the larger sequent, as required.
We prove the third property by induction on the structure of formulas. The only non-trivial case is for . In this case, the result follows straightforwardly from the induction and the fact that when . ∎
We now prove monotonicity of the function for unwindings. In fact, this holds more generally for finite (test-free) derivations of logical rules of any height.
Proposition 6 (Monotonicity of )
For be a capped unwinding for test-free, acyclic , then , for all its open leaves .
Proof
By induction on the structure of derivations. By transitivity of , it suffices to show that for the conclusion and each premise of any proof rule, . Notice that we do not need to consider (Cut) and (Subst), since these are not used in unwindings.
(WL), (WR):
If the principal formula is a relational atom the result is immediate since these do not contribute to the value of for sequents. If the principal formula is a labelled formula then the result follows by lemma 7. Items 7(1) and 7(2) gives that the value of for every label is greater for the conclusion that it is for the premise. Then, for every labelled formula common to both the premise and concluse, item 7(3) gives that its value is greater in the conclusion; therefore, the sum for the conclusion is greater than the sum for the premise. The new labelled formula in the conclusion can only increase the value of the sum.
Classical connectives:
These cases follow relatively straightforwardly. We work through the left- and right-hand cases for conjunction as an illustration.
(L):
Let denote the conclusion sequent and denote the premise sequent . First of all note that, since , we have that . Therefore, we need to show that the following inequality holds: , where . This follows directly from definition 14, which shows that they are in fact equal.
R):
Let , , and denote the conclusion sequent , the left-hand premise sequent , and the right-hand premise sequent , respectively. We first consider the result for . Here, since is the maximum of and , we have only that . But then by item 7(3), we have that the following holds for all in : ; and that for all in . Thus it suffices to show that the following inequality also holds: . By definition 14, this holds if we also have the that following inequality holds: . But this follows directly from item 7(3). The result for the right-hand premise is shown symmetrically.
∎
See 1
Proof
The sequent is test-free and acyclic. We start with the open derivation consisting of the single open leaf . A proof can be found by iteratively building capped unwindings for the currently open leaves. By lemma 5(2), all open leaves at each stage are valid. Moreover, since is test-free, so are all sequents occurring during proof-search, which contain only formulas in the Fischer-Ladner closure of . By proposition 2, each open leaf at each stage is also acyclic. By lemma 6, each unwinding is finite, and so can be built in finite time. Propositions 5 and 6 ensure that the number of labelled iterated formulas in each open leaf encountered in proof-search is bounded by . Moreover, lemma 6 ensures that the bound on the number of iterated formulas is also a bound on the number of labels occurring in the open leaves. This means that the size of the sequent in each open leaf is bounded. That is, the number of distinct open leaves encountered during proof-search is bounded, modulo label substitution. Therefore, during proof-search, if any open leaf is a substitution instance of a previously encountered sequent we can apply a substitution, convert it to a bud and assign the previously encountered node as its companion. We must eventually end up with a pre-proof after finite time. Due to the sub-formula property of all rules except (L) and (R), for any infinite path through the pre-proof there must be a path of ancestry following some consequent iterated (sub-)formula. Since all unwindings are finite, the infinite path must cycle through some unwinding an infinite number of times. Moreover, since sequents are finite, the path must go through some labelled formula in the conclusion of this unwinding an infinite number of times. By the construction of unwindings, is an iterated formula . We can therefore form a trace from this formula starting with that follows this path. Then by lemma 5(3), each segment of the trace between occurrences of this formula (of which there are infinitely many) is progressing. Thus, the pre-proof satisfies the global trace condition. ∎
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Loredana Afanasiev, Patrick Blackburn, Ioanna Dimitriou, Bertrand Gaiffe, Evan Goris, Maarten Marx, and Maarten de Rijke. PDL for ordered trees. Journal of Applied Non-Classical Logics , 15(2):115–135, 2005.
- 2[2] Luca Alberucci. The Modal μ 𝜇 \mu -calculus and the Logic of Common Knowledge . Ph D thesis, Universität Bern, 2002.
- 3[3] Philippe Balbiani and Dimiter Vakarelov. PDL with intersection of programs: a complete axiomatization. Journal of Applied Non-Classical Logics , 13(3-4):231–276, 2003.
- 4[4] Johan Van Benthem. Modal frame correspondences and fixed-points. Studia Logica , 83(1):133–155, Jun 2006.
- 5[5] James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. J. Log. Comput. , 21(6):1177–1216, 2011.
- 6[6] Facundo Carreiro and Yde Venema. PDL inside the μ 𝜇 \mu -calculus: A syntactic and an automata-theoretic characterization. In Rajeev Goré, Barteld Kooi, and Agi Kurucz, editors, Advances in Modal Logic, Volume 10 , pages 74–93. CSLI Publications, 2014.
- 7[7] Liron Cohen and Reuben N. S. Rowe. Uniform inductive reasoning in transitive closure logic via infinite descent. In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK , pages 17:1–17:16, 2018.
- 8[8] Anupam Das and Damien Pous. A cut-free cyclic proof system for kleene algebra. In Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017, Proceedings , pages 261–277, 2017.