On Induction for Diamond-Free Directed Complete Partial Orders Ievgen Ivanov Taras Shevchenko National University of Kyiv ivanov.eugen@gmail.com Abstract. A formulation of an induction principle for diamond-free di- rected complete partial orders is proposed. This principle may be useful for specification and verification of non-discrete systems using interactive proof assistant software. Keywords: Formal methods, partial order, real induction, open induc- tion. 1 Introduction Inductive proofs and recursive definitions are very useful tools in software spec- ification and verification. In particular, they are frequently used in formaliza- tions of algorithms in proof assistants such as Isabelle and Coq. This leads to a question of whether certain analogous proof methods and corresponding def- inition methods may be useful in the case of specification and verification of cyber-physical systems, in particular, using proof assistants. Since in this case one is expected to deal with formalization of properties which involve continu- ous variables, investigation of generalized inductive proof methods and recursive definitions which use a continuous parameter is relevant. Proof principles that allow one to prove a property of real numbers by an argument that is in some sense similar to mathematical induction may be called real or continuous induction principles [1–3]. An overview, literature references and applications related to this topic can be found in [1, 2]. Recently, real induction was used in differential equation invariance axioma- tization [4, 5] which extends a logic (differential dynamic logic [4]) intended for verification of hybrid systems (which may be used as mathematical models of behaviors of cyber-physical systems). The real induction principle referenced in [4] is given in [2, Theorem 2]. It states that a subset S ⊆ [a, b] (a < b are real numbers) is inductive if and only if S = [a, b]. Here a subset S ⊆ [a, b] is called inductive, if it satisfies the following properties [2]: (1) a ∈ S; (2) if a ≤ x < b, then x ∈ S implies [x, y] ⊆ S for some y > x; (3) if a < x ≤ b and [a, x) ⊆ S, then x ∈ S. A more general theorem which characterizes Dedekind-complete total orders is also given in [2]. Copyright © 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). A discussion of a question about generalization of a slightly different theorem for total orders to an induction principle for partial orders and a formulation of an induction principle for complete lattices can be found at [6]. However, in formal methods and verification, some posets of interest do not form lattices. One example is the set of partial trajectories of a nondeterminis- tic (possibly hybrid) dynamical system, defined on time intervals of the forms [0, t), [0, t], ordered by the extension relation (s1 ≤ s2 , if s2 extends s1 ), where diverging trajectories (incomparable elements) have no joins. But in this example and in some other, a poset of interest belongs to the class of diamond-free posets, i.e. posets such that there is no tuple (a, b, c, d) in which a ≤ b ≤ d, a ≤ c ≤ d, and b, c are incomparable. In this paper we will argue that Raoult’s open induction principle [7] can be used to obtain an induction principle for diamond-free directed complete partial orders (dcpos) which extends the real induction principle. 2 Preliminaries Let (X, ≤) be a subset and A ⊆ X be a subset. We will use the following notation: – < is the strict order which corresponds to ≤ ; – [a, b] is the set {x ∈ X | a ≤ x ∧ x ≤ b}; – [a, b) is the set {x ∈ X | a ≤ x ∧ x < b}; – x = sup≤ A denotes that x is the least upper bound of A in (X, ≤). We will assume that the axiom of choice holds. 3 Main Result Firstly, let us consider the following auxiliary statement. Theorem 1 (Converse open induction principle). Let (X, ≤) be a poset. Assume that X is the only directed open subset S ⊆ X which satisfies the following condition: (1) for each x ∈ X, if ∀y ∈ X(x < y ⇒ y ∈ S) holds, then x ∈ S. Then (X, ≤) is a dcpo. Proof. Suppose that (X, ≤) is not directed complete (so (X, ≤) is not chain com- plete). Then there exists a nonempty ≤-chain C ⊆ X which has no supremum in (X, ≤). Let C 0 be the directed closure of C. Let S = X\C 0 . Let us show that S satisfies the condition (1). Let x ∈ X. Assume that ∀y ∈ X(x < y ⇒ y ∈ S) holds. Suppose that x ∈ / S. Then x ∈ C 0 . The set {sup≤ C 00 | C 00 ⊆ C, C 00 6= ∅, and C 00 has a supremum} is directed closed. Then x = sup≤ C 00 for some nonempty ≤-chain C 00 ⊆ C. Let us show that C and C 00 are cofinal. Let c ∈ C. Suppose that for each c00 ∈ C 00 , c < c00 does not hold. Since C 00 ⊆ C, each element of C 00 is comparable with c. Then c is an upper bound of C 00 . Then x ≤ c. The relation x < c cannot hold, because it implies c ∈ S = X\C 0 , but c ∈ C ⊆ C 0 . Hence x = c ∈ C. Then each y ∈ C such that x < y belongs to S. This implies that x is the largest element of C. Then x = sup≤ C. This contradicts the assumption that C has no supremum. Thus there exists c00 ∈ C 00 such that c < c00 holds. Since c ∈ C is arbitrary, we conclude that C and C 00 are cofinal. Then x = sup≤ C and we get a contradiction with the assumption that C has no supremum. Thus x ∈ S. Then S satisfies the condition (1). Note that S is directed open. Then S = X. Then C 0 = ∅ and we get a contradiction with the fact that C is nonempty. Thus (X, ≤) is directed complete. t u Theorem 2 (Induction principle for diamond-free dcpos). Let (X, ≤) be a diamond-free poset. Then (X, ≤) is directed complete if and only if the only subset S ⊆ X which satisfies the conditions (1)-(2) is X: (1) for each x ∈ X, if ∀y ∈ X(x < y ⇒ y ∈ S) holds, then x ∈ S; (2) for each x ∈ X and z ∈ S such that x < z and sup≤ [x, z) = z, there exists y ∈ [x, z) such that [y, z) ⊆ S. Proof. “If”. Assume that X is the only subset of X which satisfies (1)-(2). Let us show that each directed open set S satisfies the condition (2). Let S ⊆ X be a directed open set, and x ∈ X and z ∈ S be such that x < z and sup≤ [x, z) = z. Suppose that for each y ∈ [x, z) we have [y, z)\S 6= ∅. Then the sets [x, z) and [x, z)\S are cofinal. Denote C = [x, z)\S. Then sup≤ C = z ∈ S. Moreover, C is a ≤-chain, since [x, z)\S ⊆ [x, z] and (X, ≤) is diamond-free. Since S is directed open, C ∩ S 6= ∅. We have a contradiction with the definition C = [x, z)\S. Thus there exists y ∈ [x, z) such that [y, z) ⊆ S. Thus X is the only directed open subset of X which satisfies the condition (1). Then (X, ≤) is a dcpo by Theorem 1. “Only if”. Assume that (X, ≤) is a diamond-free dcpo. Obviously, S = X satisfies 1-2. Let S ⊆ X be a set which satisfies 1-2. Let us show that S = X. Firstly, let us show that S is a directed open set. Let C be a nonempty ≤-chain such that sup≤ C = z ∈ S. Let us show that C ∩ S 6= ∅. Without loss of generality, assume that z ∈ / C. Let x be some element of C. Note that x < z. Let C1 = {y ∈ C | x ≤ y}. Then C1 is a nonempty ≤-chain. Moreover, C and C1 are cofinal, so sup≤ C1 = z. Since z ∈ / C, we have C1 ⊆ [x, z). Let y ∈ [x, z). Since sup≤ C1 = z, y is not an upper bound of C1 . Then exists c ∈ C1 such that c ≤ y does not hold. Note that c and y are not incomparable, since c, y ∈ [x, z] and (X, ≤) is diamond-free. Then y < c. Since y is arbitrary, C1 and [x, z) are cofinal. Then sup≤ [x, z) = z. Then from the condition (2) it follows that there exists y ∈ [x, z) such that [y, z] ⊆ S. Since x ≤ y < z and sup≤ C = z, there exists c ∈ C ∩ [x, z] such that c ≤ y does not hold. Note that c and y are not incomparable, because c, y ∈ [x, z] and (X, ≤) is diamond-free. Then y < c, so c ∈ [y, z] ⊆ S and C ∩ S 6= ∅. Since C is arbitrary, this implies that S is a directed open set in (X, ≤). From the condition (1) it follows that S is the set of elements which satisfy an inductive property in the sense of [7, Proposition 1.2]. Then S = X by the open induction principle [7]. t u 4 Discussion Similarly to the case of the real induction principle, the conditions (1)-(2) of Theorem 2 can be formulated as a first-order formula in a signature that has symbols for the predicate of membership in S, the relation ≤, and equality. The condition (1) states that the predicate P (x) ⇔ x ∈ S defines an induc- tive property in the terminology of [7] (which should not be confused with the notion of an inductive subset from [2]). It also corresponds to the formulation of Noetherian induction schema. The condition (2) is analogous, but somewhat weaker than the formulation of the condition [6, (POI2’)] for the opposite order relation (≤−1 ). Theorem 2 is applicable to total orders (which are diamond-free). In the special case when X is the real interval [0, 1] and ≤ is a restriction of the order, opposite to the standard order on real numbers, (X, ≤) is directed complete and the “only if” part of the statement of the theorem reduces to the statement that [0, 1] is the only subset S ⊆ [0, 1] which satisfies (1)-(2), where (1)-(2) are equivalent to statement that S is an inductive subset of [0, 1] in terms of [2]. Theorem 2 can also be applied to sets of partial trajectories of nondetermin- istic continuous-time dynamical systems, defined on time intervals of the form [0, t), [0, t], ordered by the extension relation (s1 ≤ s2 , if s2 extends s1 ), or the opposite of this relation (with the dual completeness requirement), assuming that a partial trajectory cannot extend two incomparable partial trajectories (since their domains are ⊆-comparable). 5 Conclusions We have proposed an induction principle for diamond-free directed complete partial orders. It can be considered as an extension of the real induction principle for a real interval. References 1. Clark, P.: The Instructor’s Guide to Real Induction. Mathematics Magazine 92, 136–150 (2019) 2. Clark, P.: The Instructor’s Guide to Real Induction (2012) Available at: http://arxiv.org/abs/1208.0973 3. Kalantari, I.: Induction over the Continuum. In: M. Friend, N.B. Goethe and V.S. Harizanov (eds.), Induction, Algorithmic Learning Theory, and Philosophy, 145– 154, Springer (2007) 4. Platzer, A., Yong Kiam Tan: Differential Equation Axiomatization: The Impressive Power of Differential Ghosts. In: Proc. of LICS’18, pp. 819–828 (2018) 5. Platzer, A., Yong Kiam Tan: Differential Equation Invariance Axiomatization (2019) Available at: http://arxiv.org/abs/1905.13429 6. A principle of mathematical induction for partially ordered sets with infima. – Web page: https://mathoverflow.net/questions/38238 7. Raoult J.-C.: Proving open properties by induction. Information Processing Letters 29, 19-23 (1988)