Three classes of decidable discrete linear orders with varying degrees of effectiveness are investigated. We consider how a classical order type may lie in relation to these three classes, and we characterize by their order types elements of these classes that have effective nontrivial self-embeddings.

Linear arithmetics are extensions of Presburger arithmetic () by one or more unary functions, each intended as multiplication by a fixed element (scalar), and containing the full induction schemes for their respective languages. In this paper, we construct a model of the 2‐linear arithmetic (linear arithmetic with two scalars) in which an infinitely long initial segment of “Peano multiplication” on is ‐definable. This shows, in particular, that is not model complete in contrast to theories and that are (...) known to satisfy quantifier elimination up to disjunctions of primitive positive formulas. As an application, we show that, as a discretely ordered module over the discretely ordered ring generated by the two scalars, does not have the NIP, answering negatively a question of Chernikov and Hils. (shrink)

Aggregation of variables allows to approximate a large scale dynamical system (the micro-system) involving many variables into a reduced system (the macro-system) described by a few number of global variables. Approximate aggregation can be performed when different time scales are involved in the dynamics of the micro-system. Perturbation methods enable to approximate the large micro-system by a macro-system going on at a slow time scale. Aggregation has been performed for systems of ordinary differential equations in which time is a continuous (...) variable. In this contribution, we extend aggregation methods to time-discrete models of population dynamics. Time discrete micro-models with two time scales are presented. We use perturbation methods to obtain a slow macro-model. The asymptotic behaviours of the micro and macro-systems are characterized by the main eigenvalues and the associated eigenvectors. We compare the asymptotic behaviours of both systems which are shown to be similar to a certain order. (shrink)

This paper is concerned with the event-based state and fault estimation problem for a class of linear discrete systems with randomly occurring faults and missing measurements. Different from the static event-based transmission mechanism with a constant threshold, a dynamic event-based mechanism is exploited here to regulate the threshold parameter, thus further reducing the amount of data transmission. Some mutually independent Bernoulli random variables are used to characterize the phenomena of ROFs and missing measurements. In order to simultaneously (...) estimate the system state and the fault signals, the main attention of this paper is paid to the design of recursive filter; for example, for all DETM, ROFs, and missing measurements, an upper bound for the estimation error covariance is ensured and the relevant filter gain matrix is designed by minimizing the obtained upper bound. Moreover, the rigorous mathematical analysis is carried out for the exponential boundedness of the estimation error. It is clear that the developed algorithms are dependent on the threshold parameters and the upper bound together with the probabilities of missing measurements and ROFs. Finally, a numerical example is provided to indicate the effectiveness of the presented estimation schemes. (shrink)

In this article we find some sufficient and some necessary ${\Sigma^1_1}$ -conditions with oracles for a model to be resplendent or chronically resplendent. The main tool of our proofs is internal arguments, that is analogues of classical theorems and model-theoretic constructions conducted inside a model of first-order Peano Arithmetic: arithmetised back-and-forth constructions and versions of the arithmetised completeness theorem, namely constructions of recursively saturated and resplendent models from the point of view of a model of arithmetic. These internal arguments (...) are used in conjunction with Pabion’s theorem that ensures that certain oracles are coded in a sufficiently saturated model of arithmetic. Examples of applications are provided for the theories of dense linear orders and of discrete linear orders. These results are then generalised to other ω-categorical theories and theories with a unique countable recursively saturated model. (shrink)

In constructive mathematics it is of interest to consider a more general, but classically equivalent, notion of linear order, a so-called pseudo-order. The prime example is the order of the constructive real numbers. We examine two kinds of constructive completions of pseudo-orders: order completions of pseudo-orders and Cauchy completions of ordered groups and fields. It is shown how these can be predicatively defined in type theory, also when the underlying set is non-discrete. Provable choice (...) principles, in particular a generalisation of dependent choice, are used for showing set-representability of cuts. (shrink)

The first-order temporal logics with □ and ○ of time structures isomorphic to ω (discrete linear time) and trees of ω-segments (linear time with branching gaps) and some of its fragments are compared: the first is not recursively axiomatizable. For the second, a cut-free complete sequent calculus is given, and from this, a resolution system is derived by the method of Maslov.

The paper aims at providing the multi-modal propositional logic LTK with a sound and complete axiomatisation. This logic combines temporal and epistemic operators and focuses on m odeling the behaviour of a set of agents operating in a system on the background of a temporal framework. Time is represented as linear and discrete, whereas knowledge is modeled as an S5-like modality. A further modal operator intended to represent environment knowledge is added to the system in order to (...) achieve the expressive power sufficient to describe the piece of information available to the agents at each moment in the flow of time. (shrink)

The paper studies the logic TL(NBox+-wC) – logic of discrete linear time with current time point clusters. Its language uses modalities Diamond+ (possible in future) and Diamond- (possible in past) and special temporal operations, – Box+w (weakly necessary in future) and Box-w (weakly necessary in past). We proceed by developing an algorithm recognizing theorems of TL(NBox+-wC), so we prove that TL(NBox+-wC) is decidable. The algorithm is based on reduction of formulas to inference rules and converting the rules in (...) special reduced normal form, and, then, on checking validity of such rules in models of singleexponential size in the rules. Also we consider the admissibility problem for TL(NBox+-wC) and show how to reduce the problem for admissibility to the decidability of TL(NBox+-wC) itself using definable universal modalities. (shrink)

A totally ordered group G is essentially periodic if for every definable non-trivial convex subgroup H of G every definable subset of G is equal to a finite union of cosets of subgroups of G on some interval containing an end segment of H; it is coset-minimal if all definable subsets are equal to a finite union of cosets, intersected with intervals. We study definable sets and functions in such groups, and relate them to the quasi-o-minimal groups introduced in Belegradek (...) et al. . Main results: An essentially periodic group G is abelian; if G is discrete, then definable functions in one variable are ultimately piecewise linear. A group such that every model elementarily equivalent to it is coset-minimal is quasi-o-minimal , and its definable functions in one variable are piecewise linear. (shrink)

We deal with the design problem of nonfragile state estimator for discrete-time genetic regulatory networks with time-varying delays and randomly occurring uncertainties. In particular, the norm-bounded uncertainties enter into the GRNs in random ways in order to reflect the characteristic of the modelling errors, and the so-called randomly occurring uncertainties are characterized by certain mutually independent random variables obeying the Bernoulli distribution. The focus of the paper is on developing a new nonfragile state estimation method to estimate the (...) concentrations of the mRNA and the protein for considered uncertain delayed GRNs, where the randomly occurring estimator gain perturbations are allowed. By constructing a Lyapunov-Krasovskii functional, a delay-dependent criterion is obtained in terms of linear matrix inequalities by properly using the discrete-time Wirtinger-based inequality and reciprocally convex combination approach as well as the free-weighting matrix method. It is shown that the proposed method ensures that the estimation error dynamics is globally asymptotically stable and the desired estimator parameter is designed via the solutions to certain LMIs. Finally, we provide two numerical examples to illustrate the feasibility and validity of the proposed estimation results. (shrink)

ABSTRACT In this paper we present a new semantic approach for propositional linear temporal logic with discrete time, strongly based in the well-order of IN (the set of natural numbers). We consider temporal connectives which express precedence, posteriority and simultaneity, and they provide a family of expressively complete temporal logics. The selection of the new semantics and connectives used in this work was principally to obtain a suitable executable temporal logic, which can be used for the specification (...) and control of process behaviour in discrete time in a similar way to thai presented by D. Gabbay in [GAB 89], Our new approach has two advantages: firstly, the connectives are defined intuitively so that they have interpretations which relate to properties of interest in real systems; secondly, it provides a new semantics that facilitates simpler proofs of many valid formulas and metatheorems. To confirm this second advantage, we use our semantics to give a formal proof of the Separation Theorem for one of these logics (specifically LN3). The great interest of this Separation Theorem for the executable temporal logic is emphasised by D. Gabbay in [GAB 89], [GAB 88]. (shrink)

We develop a timeout extension of propositional linear temporal logic to specify timing properties of timeout-based models of real-time systems. A timeout is used to model the execution of an action marking the end of a delay. With a view to expressing such timeout constraints, ToLTL uses a dynamic variable to abstract the timeout behaviour in addition to a variable which captures the global clock and some static timing variables which record time instances when discrete events occur. We (...) propose a corresponding timeout tableau for satisfiability checking of the ToLTL formulas. Further we prove that the validity checking for such an extended logic remains PSPACE-complete. Under discrete time semantics, with bounded timeout increments, the model-checking problem which verifies if a ToLTL-formula holds in a timeout Kripke structure is also shown to be PSPACE complete. We further prove that ToLTL, when interpreted over discrete time, can be embedded in the monadic second-order logic with.. (shrink)

O-minimal structures have long been thought to occupy the base of a hierarchy of ordered structures, in analogy with the role that strongly minimal structures play with respect to stable theories. This is the first in an anticipated series of papers whose aim is the development of model theory for ordered structures of rank greater than one. A class of ordered structures to which a notion of finite rank can be assigned, the decomposable structures, is introduced here. These include all (...) ordered structures definable in o-minimal structures. The principal result in this paper, Theorem 5.1, asserts roughly that a decomposable structure [Formula: see text] can be partitioned into finitely many definable subsets such that on each set the restriction of < is a "twisted lexicographic" order. As a consequence, for all n and linear orders ≺ definable on a subset X ⊆ Mn in an o-minimal structure [Formula: see text], there is a definable partition of X such that the restriction of ≺ to each set in the partition is "lexicographic". (shrink)

It is shown that the infinite-valued first-order Gödel logic G° based on the set of truth values {1/k: k ε w {0}} U {0} is not r.e. The logic G° is the same as that obtained from the Kripke semantics for first-order intuitionistic logic with constant domains and where the order structure of the model is linear. From this, the unaxiomatizability of Kröger's temporal logic of programs (even of the fragment without the nexttime operator O) and (...) of the authors' temporal logic of linear discrete time with gaps follows. (shrink)

A successivity in a linear order is a pair of elements with no other elements between them. A recursive linear order with recursive successivities U is recursively categorical if every recursive linear order with recursive successivities isomorphic to U is in fact recursively isomorphic to U . We characterize those recursive linear orders with recursive successivities that are recursively categorical as precisely those with order type k 1 + g 1 + k (...) 2 + g 2 +…+ g n -1 + k n where each k n is a finite order type, non-empty for i ϵ{2,…, n -1} and each g i is an order type from among {ω,ω * ,ω+ω * }∪{ k ·η: k. (shrink)

LetEbe a computably enumerable equivalence relation on the setωof natural numbers. We say that the quotient set$\omega /E$realizesa linearly ordered set${\cal L}$if there exists a c.e. relation ⊴ respectingEsuch that the induced structure is isomorphic to${\cal L}$. Thus, one can consider the class of all linearly ordered sets that are realized by$\omega /E$; formally,${\cal K}\left = \left\{ {{\cal L}\,|\,{\rm{the}}\,{\rm{order}}\, - \,{\rm{type}}\,{\cal L}\,{\rm{is}}\,{\rm{realized}}\,{\rm{by}}\,E} \right\}$. In this paper we study the relationship between computability-theoretic properties ofEand algebraic properties of linearly ordered sets (...) realized byE. One can also define the following pre-order$ \le _{lo} $on the class of all c.e. equivalence relations:$E_1 \le _{lo} E_2 $if every linear order realized byE1is also realized byE2. Following the tradition of computability theory, thelo-degrees are the classes of equivalence relations induced by the pre-order$ \le _{lo} $. We study the partially ordered set oflo-degrees. For instance, we construct various chains and anti-chains and show the existence of a maximal element among thelo-degrees. (shrink)

Let ⪯R be the preorder of embeddability between countable linear orders colored with elements of Rado's partial order . We show that ⪯R has fairly high complexity with respect to Borel reducibility , although its exact classification remains open.

When a linear order has an order preserving surjection onto each of its suborders, we say that it is strongly surjective. We prove that the set of countable strongly surjective linear orders is a [Formula: see text]-complete set. Using hypotheses beyond ZFC, we prove the existence of uncountable strongly surjective orders.

We address the following question: Can we expand an NIP theory by adding a linear order such that the expansion is still NIP? Easily, if acl(A)= A for all A, then this is true. Otherwise, we give counterexamples. More precisely, there is a totally categorical theory for which every expansion by a linear order has IP. There is also an ω-stable NDOP theory for which every expansion by a linear order interprets pseudofinite arithmetic.

A statement of hyperarithmetic analysis is a sentence of second order arithmetic S such that for every Y⊆ω, the minimum ω-model containing Y of RCA0 + S is HYP, the ω-model consisting of the sets hyperarithmetic in Y. We provide an example of a mathematical theorem which is a statement of hyperarithmetic analysis. This statement, that we call INDEC, is due to Jullien [13]. To the author's knowledge, no other already published, purely mathematical statement has been found with this (...) property until now. We also prove that, over RCA0, INDEC is implied by [Formula: see text] and implies ACA0, but of course, neither ACA0, nor ACA 0+ imply it. We introduce five other statements of hyperarithmetic analysis and study the relations among them. Four of them are related to finitely-terminating games. The fifth one, related to iterations of the Turing jump, is strictly weaker than all the other statements that we study in this paper, as we prove using Steel's method of forcing with tagged trees. (shrink)

We consider certain linear orders with a function on them, and discuss for which types of functions the resulting structure is or is not computably categorical. Particularly, we consider computable copies of the rationals with a fixed-point free automorphism, and also ω with a non-decreasing function.

We investigate logical consequence in temporal logics in terms of logical consecutions. i.e., inference rules. First, we discuss the question: what does it mean for a logical consecution to be 'correct' in a propositional logic. We consider both valid and admissible consecutions in linear temporal logics and discuss the distinction between these two notions. The linear temporal logic LDTL, consisting of all formulas valid in the frame 〈L, ≤, ≥〉 of all integer numbers, is the prime object of (...) our investigation. We describe consecutions admissible LDTL in a semantic way—via consecutions valid in special temporal Kripke/Hintikka models. Then we state that any temporal inference rule has a reduced normal form which is given in terms of uniform formulas of temporal degree 1. Using these facts and enhanced semantic techniques we construct an algorithm, which recognizes consecutions admissible in LDTL. Also, we note that using the same technique it follows that the linear temporal logic L (N) of all natural numbers is also decidable w.r.t. inference rules. So, we prove that both logics LDTL and L (N) are decidable w.r.t. admissible consecutions. In particular, as a consequence, they both are decidable (Known fact), and the given deciding algorithms are explicit. (shrink)

This commentary discusses the division of labor between syntax and phonology, starting with the parallel model of grammar developed by Jackendoff. It is proposed that linear, left-to-right order of linguistic items is not represented in syntax, but in phonology. Syntax concerns the abstract relations of categories alone. All components of grammar contribute to linear order, by means of the interface rules.

Numerous results about capturing complexity classes of queries by means of logical languages work for ordered structures only, and deal with non-generic, or order-dependent, queries. Recent attempts to improve the situation by characterizing wide classes of finite models where linear order is definable by certain simple means have not been very promising, as certain commonly believed conjectures were recently refuted (Dawar's Conjecture). We take on another approach that has to do with normalization of a given order (...) (rather than with defining a linear order from scratch). To this end, we show that normalizability of linear order is a strictly weaker condition than definability (say, in the least fixpoint logic), and still allows for extending Immerman-Vardi-style results to generic queries. It seems to be the weakest such condition. We then conjecture that linear order is normalizable in the least fixpoint logic for any finitely axiomatizable class of rigid structures. Truth of this conjecture, which is a strengthened version of Stolboushkin's conjecture, would have the same practical implications as Dawar's Conjecture. Finally, we suggest a series of reductions of the two conjectures to specialized classes of graphs, which we believe should simplify further work. (shrink)

We characterize the linear order types $\tau $ with the property that given any countable linear order $\mathcal {L}$, $\tau \cdot \mathcal {L}$ is a computable linear order iff $\mathcal {L}$ is a computable linear order, as exactly the finite nonempty order types.

A wide family of many-valued logics—for instance, those based on the weak Kleene algebra—includes a non-classical truth-value that is ‘contaminating’ in the sense that whenever the value is assigned to a formula φ⁠, any complex formula in which φ appears is assigned that value as well. In such systems, the contaminating value enjoys a wide range of interpretations, suggesting scenarios in which more than one of these interpretations are called for. This calls for an evaluation of systems with multiple contaminating (...) values. In this paper, we consider the countably infinite family of multiple-conclusion consequence relations in which classical logic is enriched with one or more contaminating values whose behavior is determined by a linear ordering between them. We consider some motivations and applications for such systems and provide general characterizations for all consequence relations in this family. Finally, we provide sequent calculi for a pair of four-valued logics including two linearly ordered contaminating values before defining two-sided sequent calculi corresponding to each of the infinite family of many-valued logics studied in this paper. (shrink)

We study the first-order theories of some natural and important classes of coloured trees, including the four classes of trees whose paths have the order type respectively of the natural numbers, the integers, the rationals, and the reals. We develop a technique for approximating a tree as a suitably coloured linear order. We then present the first-order theories of certain classes of coloured linear orders and use them, along with the approximating technique, to establish (...) complete axiomatisations of the four classes of trees mentioned above. (shrink)

The decision problem for positively quantified formulae in the theory of linearly ordered Heyting algebras is known, as a special case of work of Kreisel, to be solvable; a simple solution is here presented, inspired by related ideas in Gödel-Dummett logic.

We introduce the logics GLP Λ, a generalization of Japaridze’s polymodal provability logic GLP ω where Λ is any linearly ordered set representing a hierarchy of provability operators of increasing strength. We shall provide a reduction of these logics to GLP ω yielding among other things a finitary proof of the normal form theorem for the variable-free fragment of GLP Λ and the decidability of GLP Λ for recursive orderings Λ. Further, we give a restricted axiomatization of the variable-free fragment (...) of GLP Λ. (shrink)

Linguistic category learning has been shown to be highly sensitive to linear order, and depending on the task, differentially sensitive to the information provided by preceding category markers (premarkers, e.g., gendered articles) or succeeding category markers (postmarkers, e.g., gendered suffixes). Given that numerous systems for marking grammatical categories exist in natural languages, it follows that a better understanding of these findings can shed light on the factors underlying this diversity. In two discriminative learning simulations and an artificial language (...) learning experiment, we identify two factors that modulate linear order effects in linguistic category learning: category structure and the level of abstraction in a category hierarchy. Regarding category structure, we find that postmarking brings an advantage for learning category diagnostic stimulus dimensions, an effect not present when categories are non‐confusable. Regarding levels of abstraction, we find that premarking of super‐ordinate categories (e.g., noun class) facilitates learning of subordinate categories (e.g., nouns). We present detailed simulations using a plausible candidate mechanism for the observed effects, along with a comprehensive analysis of linear order effects within an expectation‐based account of learning. Our findings indicate that linguistic category learning is differentially guided by pre‐ and postmarking, and that the influence of each is modulated by the specific characteristics of a given category system. (shrink)

Linguistic category learning has been shown to be highly sensitive to linear order, and depending on the task, differentially sensitive to the information provided by preceding category markers (premarkers, e.g., gendered articles) or succeeding category markers (postmarkers, e.g., gendered suffixes). Given that numerous systems for marking grammatical categories exist in natural languages, it follows that a better understanding of these findings can shed light on the factors underlying this diversity. In two discriminative learning simulations and an artificial language (...) learning experiment, we identify two factors that modulate linear order effects in linguistic category learning: category structure and the level of abstraction in a category hierarchy. Regarding category structure, we find that postmarking brings an advantage for learning category diagnostic stimulus dimensions, an effect not present when categories are non‐confusable. Regarding levels of abstraction, we find that premarking of super‐ordinate categories (e.g., noun class) facilitates learning of subordinate categories (e.g., nouns). We present detailed simulations using a plausible candidate mechanism for the observed effects, along with a comprehensive analysis of linear order effects within an expectation‐based account of learning. Our findings indicate that linguistic category learning is differentially guided by pre‐ and postmarking, and that the influence of each is modulated by the specific characteristics of a given category system. (shrink)

Pseudo-BCK-algebras are a non-commutative generalization of well-known BCK-algebras. The paper describes a situation when a linearly ordered pseudo-BCK-algebra is an ordinal sum of linearly ordered cone algebras. In addition, we present two identities giving such a possibility of the decomposition and axiomatize the residuation subreducts of representable pseudo-hoops and pseudo-BL-algebras.

Cohesive powersof computable structures are effective analogs of ultrapowers, where cohesive sets play the role of ultrafilters. Let$\omega $,$\zeta $, and$\eta $denote the respective order-types of the natural numbers, the integers, and the rationals when thought of as linear orders. We investigate the cohesive powers of computable linear orders, with special emphasis on computable copies of$\omega $. If$\mathcal {L}$is a computable copy of$\omega $that is computably isomorphic to the usual presentation of$\omega $, then every cohesive power of$\mathcal (...) {L}$has order-type$\omega + \zeta \eta $. However, there are computable copies of$\omega $, necessarily not computably isomorphic to the usual presentation, having cohesive powers not elementarily equivalent to$\omega + \zeta \eta $. For example, we show that there is a computable copy of$\omega $with a cohesive power of order-type$\omega + \eta $. Our most general result is that if$X \subseteq \mathbb {N} \setminus \{0\}$is a Boolean combination of$\Sigma _2$sets, thought of as a set of finite order-types, then there is a computable copy of$\omega $with a cohesive power of order-type$\omega + \boldsymbol {\sigma }(X \cup \{\omega + \zeta \eta + \omega ^*\})$, where$\boldsymbol {\sigma }(X \cup \{\omega + \zeta \eta + \omega ^*\})$denotes the shuffle of the order-types inXand the order-type$\omega + \zeta \eta + \omega ^*$. Furthermore, ifXis finite and non-empty, then there is a computable copy of$\omega $with a cohesive power of order-type$\omega + \boldsymbol {\sigma }(X)$. (shrink)

A low linear order with no computable copy constructed by C. Jockusch and R. Soare has Hausdorff rank equal to $2$. In this regard, the question arises, how simple can be a low linear order with no computable copy from the point of view of the linear order type? The main result of this work is an example of a low strong $\eta $ -representation with no computable copy that is the simplest possible example.

In this paper we define the notion of -linearity for and discuss interpretability (and noninterpretability) of -linear orders in structures and theories.

We re-express a previous general result in a way which seems easier to remember, using the terminology of infinite games. We show how this can be applied to construct recursive linear orderings, showing, for example, that if there is a ▵ 0 2β + 1 linear ordering of type τ, then there is a recursive ordering of type ω β · τ.