On Induction for Diamond-Free Directed Complete Partial Orders Ievgen Ivanov ivanov.eugen@gmail.com 0 Taras Shevchenko National University of Kyiv

A formulation of an induction principle for diamond-free directed complete partial orders is proposed. This principle may be useful for speci cation and veri cation of non-discrete systems using interactive proof assistant software.

 Formal methods partial order real induction open induction Introduction

Inductive proofs and recursive de nitions are very useful tools in software speci cation and veri cation. In particular, they are frequently used in formalizations of algorithms in proof assistants such as Isabelle and Coq. This leads to a question of whether certain analogous proof methods and corresponding definition methods may be useful in the case of speci cation and veri cation of cyber-physical systems, in particular, using proof assistants. Since in this case one is expected to deal with formalization of properties which involve continuous variables, investigation of generalized inductive proof methods and recursive de nitions 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 di erential equation invariance axiomatization [4, 5] which extends a logic (di erential dynamic logic [4]) intended for veri cation 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 satis es the following properties [2]: ( 1 ) a 2 S; ( 2 ) if a x < b, then x 2 S implies [x; y] S for some y > x; ( 3 ) if a < x b and [a; x) S, then x 2 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 di erent 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 veri cation, some posets of interest do not form lattices. One example is the set of partial trajectories of a nondeterministic (possibly hybrid) dynamical system, de ned 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 fx 2 X j a x ^ x bg; { [a; b) is the set fx 2 X j a x ^ x < bg; { 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 satis es the following condition: ( 1 ) for each x 2 X, if 8y 2 X(x < y ) y 2 S) holds, then x 2 S.

Then (X; ) is a dcpo.

Proof. Suppose that (X; ) is not directed complete (so (X; ) is not chain complete). Then there exists a nonempty -chain C X which has no supremum in (X; ). Let C0 be the directed closure of C. Let S = XnC0. Let us show that S satis es the condition ( 1 ).

Let x 2 X. Assume that 8y 2 X(x < y ) y 2 S) holds. Suppose that x 2= S. Then x 2 C0. The set fsup C00 j C00 C; C00 6= ;; and C00 has a supremumg is directed closed. Then x = sup C00 for some nonempty -chain C00 C. Let us show that C and C00 are co nal. Let c 2 C. Suppose that for each c00 2 C00, c < c00 does not hold. Since C00 C, each element of C00 is comparable with c. Then c is an upper bound of C00. Then x c. The relation x < c cannot hold, because it implies c 2 S = XnC0, but c 2 C C0. Hence x = c 2 C. Then each y 2 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 2 C00 such that c < c00 holds. Since c 2 C is arbitrary, we conclude that C and C00 are co nal. Then x = sup C and we get a contradiction with the assumption that C has no supremum. Thus x 2 S.

Then S satis es the condition ( 1 ). Note that S is directed open. Then S = X. Then C0 = ; and we get a contradiction with the fact that C is nonempty.

Thus (X; ) is directed complete. tu 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 satis es the conditions ( 1 )-( 2 ) is X: ( 1 ) for each x 2 X, if 8y 2 X(x < y ) y 2 S) holds, then x 2 S; ( 2 ) for each x 2 X and z 2 S such that x < z and sup [x; z) = z, there exists y 2 [x; z) such that [y; z) S.

Proof. \If". Assume that X is the only subset of X which satis es ( 1 )-( 2 ).

Let us show that each directed open set S satis es the condition ( 2 ). Let S X be a directed open set, and x 2 X and z 2 S be such that x < z and sup [x; z) = z. Suppose that for each y 2 [x; z) we have [y; z)nS 6= ;. Then the sets [x; z) and [x; z)nS are co nal. Denote C = [x; z)nS. Then sup C = z 2 S. Moreover, C is a -chain, since [x; z)nS [x; z] and (X; ) is diamond-free. Since S is directed open, C \ S 6= ;. We have a contradiction with the de nition C = [x; z)nS. Thus there exists y 2 [x; z) such that [y; z) S.

Thus X is the only directed open subset of X which satis es the condition ( 1 ). Then (X; ) is a dcpo by Theorem 1.

\Only if". Assume that (X; ) is a diamond-free dcpo. Obviously, S = X satis es 1-2. Let S X be a set which satis es 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 2 S.

Let us show that C \ S 6= ;. Without loss of generality, assume that z 2= C. Let x be some element of C. Note that x < z.

Let C1 = fy 2 C j x yg. Then C1 is a nonempty -chain. Moreover, C and C1 are co nal, so sup C1 = z. Since z 2= C, we have C1 [x; z).

Let y 2 [x; z). Since sup C1 = z, y is not an upper bound of C1. Then exists c 2 C1 such that c y does not hold. Note that c and y are not incomparable, since c; y 2 [x; z] and (X; ) is diamond-free. Then y < c.

Since y is arbitrary, C1 and [x; z) are co nal. Then sup [x; z) = z.

Then from the condition ( 2 ) it follows that there exists y 2 [x; z) such that [y; z] S. Since x y < z and sup C = z, there exists c 2 C \ [x; z] such that c y does not hold. Note that c and y are not incomparable, because c; y 2 [x; z] and (X; ) is diamond-free. Then y < c, so c 2 [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].

 Discussion

Similarly to the case of the real induction principle, the conditions ( 1 )-( 2 ) of Theorem 2 can be formulated as a rst-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 2 S de nes an inductive 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 satis es ( 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 nondeterministic continuous-time dynamical systems, de ned 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.

 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: Di erential Equation Axiomatization: The Impressive Power of Di erential Ghosts . In: Proc. of LICS'18 , pp. 819 { 828 ( 2018 ) 5. Platzer , A. , Yong Kiam Tan: Di erential Equation Invariance Axiomatization ( 2019 ) Available at: http://arxiv.org/abs/ 1905 .13429 6. A principle of mathematical induction for partially ordered sets with in ma . { Web page: https://mathover ow. net/questions/38238 7. Raoult J.-C. : Proving open properties by induction . Information Processing Letters 29 , 19 - 23 ( 1988 )