=Paper=
{{Paper
|id=Vol-2732/20200070
|storemode=property
|title=On Induction for Diamond-Free Directed Complete Partial Orders
|pdfUrl=https://ceur-ws.org/Vol-2732/20200070.pdf
|volume=Vol-2732
|authors=Ievgen Ivanov
|dblpUrl=https://dblp.org/rec/conf/icteri/Ivanov20
}}
==On Induction for Diamond-Free Directed Complete Partial Orders==
https://ceur-ws.org/Vol-2732/20200070.pdf
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)