Deontic logic is devoted to the study of logical properties of normative predicates such as permission, obligation and prohibition. Since it is usual to apply these predicates to actions, many deontic logicians have proposed formalisms where actions and action combinators are present. Some standard action combinators are action conjunction, choice between actions and not doing a given action. These combinators resemble boolean operators, and therefore the theory of boolean algebra offers a well-known athematical framework to study the properties (...) of the classic deontic operators when applied to actions. In his seminal work, Segerberg uses constructions coming from boolean algebras to formalize the usual deontic notions. Segerberg’s work provided the initial step to understand logical properties of deontic operators when they are applied to actions. In the last years, other authors have proposed related logics. In this chapter we introduce Segerberg’s work, study related formalisms and investigate further challenges in this area. (shrink)

A set F of Boolean functions is said to be functionally complete if every Boolean function is definable by combining functions in F. Post clarified when a set of Boolean functions is functionally complete (with respect to classical semantics). In this paper, by extending Post’s theorem, we clarify when a set of Boolean functions is functionally complete with respect to Kripke semantics.

We address the general problem of determining the validity of boolean combinations of equalities and inequalities between real-valued expressions. In particular, we consider methods of establishing such assertions using only restricted forms of distributivity. At the same time, we explore ways in which “local'’ decision or heuristic procedures for fragments of the theory of the reals can be amalgamated into global ones. Let $Tadd[QQ]$ be the first-order theory of the real numbers in the language with symbols $0, 1, (...) +, -. (shrink)

Given current data, only a few binary Boolean operators are expressed in lexically simple fashion in the world's languages: and, or, nor. These do not occur in every combination, for example, nor is not observed by itself. To explain these cross‐linguistic patterns, we propose an encoding of Boolean operators as update procedures to accept or reject information in a context. We define a measure of conceptual simplicity for such updates, on which attested operators are conceptually simpler than the (...) remaining Booleans. Moreover, we show that language evolution selects for the attested lexical inventories by minimizing the complexity of using a lexical inventory compositionally to convey precise information. (shrink)

The Boolean many-valued approach to vagueness is similar to the infinite-valued approach embraced by fuzzy logic in the respect in which both approaches seek to solve the problems of vagueness by assigning to the relevant sentences many values between falsity and truth, but while the fuzzy-logic approach postulates linearly-ordered values between 0 and 1, the Boolean approach assigns to sentences values in a many-element complete Boolean algebra. On the modal-precisificational approach represented by Kit Fine, if a sentence (...) is indeterminate in truth value in some world, it is taken to be true in one precisified world accessible from that world and false in another. This paper points to a way to unify these two approaches to vagueness by showing that Fine’s version of the modal-precisificational approach can be combined with the Boolean many-valued approach instead of supervaluationism, one of the most popular approaches to vagueness. (shrink)

Since antiquity two different negations in natural languages have been noted: predicate negation (not honest) and predicate term negation (dishonest). The extensive literature offers no models. We propose category-theoretic models with two distinct negation operators, neither of them in general Boolean. We study combinations of the two (not dishonest) and sentential counterparts of each. We emphasize the relevance of our work for the theory of cognition.

Since antiquity two different negations in natural languages have been noted: predicate negation and predicate term negation . The extensive literature offers no models. We propose category-theoretic models with two distinct negation operators, neither of them in general Boolean. We study combinations of the two and sentential counterparts of each. We emphasize the relevance of our work for the theory of cognition.

Boolean connexive logic is an extension of Boolean logic that is closed under Modus Ponens and contains Aristotle’s and Boethius’ theses. According to these theses a sentence cannot imply its negation and the negation of a sentence cannot imply the sentence; and if the antecedent implies the consequent, then the antecedent cannot imply the negation of the consequent and if the antecedent implies the negation of the consequent, then the antecedent cannot imply the consequent. Such a logic was (...) first introduced by Jarmużek and Malinowski, by means of so-called relating semantics and tableau systems. Subsequently its modal extension was determined by means of the combination of possible-worlds semantics and relating semantics. In the following article we present axiomatic systems of some basic and modal Boolean connexive logics. Proofs of completeness will be carried out using canonical models defined with respect to maximal consistent sets. (shrink)

The theorem of the title is proven, solving an old question of Remmel. The method of proof uses an algebraic technique of Remmel-Vaught combined with a complex tree of strategies argument where the true path is needed to figure out the final isomorphism.

We introduce a family of tableau calculi for deontic action logics based on finite boolean algebras, these logics provide deontic operators which are applied to a finite number of actions ; furthermore, in these formalisms, actions can be combined by means of boolean operators, this provides an expressive algebra of actions. We define a tableau calculus for the basic logic and then we extend this calculus to cope with extant variations of this formalism; we prove the soundness and (...) completeness of these proof systems. In addition, we investigate the computational complexity of the satisfiability problem for DAL and its extensions; we show this problem is NP-complete when the number of actions considered is fixed, and it is \-Hard when the number of actions is taken as an extra parameter. The tableau systems introduced here can be implemented in PSPACE, this seems reasonable taking into consideration the computational complexity of the logics. (shrink)

Neoclassical economic theory, which still dominates the science, has proven inadequate to predict financial crises. In an increasingly globalised world, the consequences of that inadequacy are likely to become more severe. This article attributes much of the difficulty to an emphasis on equilibrium as an idealised property of economic systems. Alternatively, this article proposes that actual economies are typically out of balance, and that any equilibrium which may exist is transitory. That single changed assumption is central to complexity economics, a (...) view which is presented in detail. It is suggested that economic crises will be most effectively avoided when economists utilise methods, grounded in complexity theory, which can identify threat in an early stage. As a programmatic example, the use of Agent-Based Models (ABMs) combined with Boolean networks (BNs), is defended as a promising method for recognising vulnerability. (shrink)

Checking the equivalence of two Boolean functions, or combinational circuits modeled as Boolean functions, is often desired when reliable and correct hardware components are required. The most common approaches to equivalence checking are based on simulation and model checking, which are constrained due to the popular memory and state explosion problems. Furthermore, such tools are often not user-friendly, thereby making it tedious to check the equivalence of large formulas or circuits. An alternative is to use mathematical tools, called (...) interactive theorem provers, to prove the equivalence of two circuits; however, this requires human effort and expertise to write multiple output functions and carry out interactive proof of their equivalence. In this paper, we define two simple, one formal and the other informal, gate-level hardware description languages, design and develop a formal automatic combinational circuit equivalence checker tool, and test and evaluate our tool. The tool CoCEC is based on human-assisted theorem prover Coq, yet it checks the equivalence of circuit descriptions purely automatically through a human-friendly user interface. It either returns a machine-readable proof of circuits’ equivalence or a counterexample of their inequality. The interface enables users to enter or load two circuit descriptions written in an easy and natural style. It automatically proves, in few seconds, the equivalence of circuits with as many as 45 variables. CoCEC has a mathematical foundation, and it is reliable, quick, and easy to use. The tool is intended to be used by digital logic circuit designers, logicians, students, and faculty during the digital logic design course. (shrink)

We prove that PTIME generalized quantifiers are closed under Boolean operations, iteration, cumulation and resumption. -/- .

We define a formula φ in a first-order language L , to be an equation in a category of L -structures K if for any H in K , and set p = {φ;i ϵI, a i ϵ H} there is a finite set I 0 ⊂ I such that for any f : H → F in K , ▪. We say that an elementary first-order theory T which has the amalgamation property over substructures is equational if every quantifier-free (...) formula is equivalent in T to a boolean combination of equations in Mod, the category of models of T with embeddings for morphisms. Thus, we develop a theory of independence with respect to equations in general categories of structures, which is similar to the one introduced in stability but which, in our context, has an algebraic character. (shrink)

The Logic & Structure project is about the language of mathematical logic and how it can be of use in the visual arts. It involves a conversation between a mathematical logician and a group of artists. The project is ongoing, and this is a report on its first two phases. This text has two parts. The first, “Logic”, is a short introduction to certain aspects of logic, as it was presented to the participants. The second part, “Structures”, describes some of (...) the outcomes.The inspiration for the project comes from modern model theory whose advances revealed the extent to which formal methods may be helpful in describing and analysing mathematical structures. While the structures that are studied are often immensely complex, the formal language in which their properties can be expressed is simple. Its syntax is precisely defined and well understood, and this understanding often successfully guides us in our explorations of the rich world of mathematical objects. Our goal is to see the extent to which a similar approach could be of value when talking about works of art as structures. To this end, one could try to describe existing art objects in terms of suitably chosen formal languages, but we follow a reverse route. The language is described first, and the participating artists are asked to come up with artwork in which formal elements and their relations are chosen in advance, making it easier to identify those features of the created pieces that can be formally expressed. In other words, we are not thinking of applying formal methods to create art; rather we want to begin with samples that can serve as material for discussion. (shrink)

We study the degrees of unsolvability of sets which are cohesive . We answer a question raised by the first author in 1972 by showing that there is a cohesive set A whose degree a satisfies a' = 0″ and hence is not high. We characterize the jumps of the degrees of r-cohesive sets, and we show that the degrees of r-cohesive sets coincide with those of the cohesive sets. We obtain analogous results for strongly hyperimmune and strongly hyperhyperimmune sets (...) in place of r-cohesive and cohesive sets, respectively. We show that every strongly hyperimmune set whose degree contains either a Boolean combination of ∑2 sets or a 1-generic set is of high degree. We also study primitive recursive analogues of these notions and in this case we characterize the corresponding degrees exactly. MSC: 03D30, 03D55. (shrink)

Three central combinatorial properties in set theory are the tree property, the approachability property and stationary reflection. We prove the mutual independence of these properties by showing that any of their eight Boolean combinations can be forced to hold at${\kappa ^{ + + }}$, assuming that$\kappa = {\kappa ^{ < \kappa }}$and there is a weakly compact cardinal aboveκ.If in additionκis supercompact then we can forceκto be${\aleph _\omega }$in the extension. The proofs combine the techniques of adding and (...) then destroying a nonreflecting stationary set or a${\kappa ^{ + + }}$-Souslin tree, variants of Mitchell’s forcing to obtain the tree property, together with the Prikry-collapse poset for turning a large cardinal into${\aleph _\omega }$. (shrink)

In this paper we introduce the notion of a first order topological structure, and consider various possible conditions on the complexity of the definable sets in such a structure, drawing several consequences thereof.Our aim is to develop, for a restricted class of unstable theories, results analogous to those for stable theories. The “material basis” for such an endeavor is the analogy between the field of real numbers and the field of complex numbers, the former being a “nicely behaved” unstable structure (...) and the latter the archetypal stable structure. In this sense we try here to situate our work ono-minimal structures [PS] in a general topological context. Note, however, that thep-adic numbers, and structures definable therein, will also fit into our analysis.In the remainder of this section we discuss several ways of studying topological structures model-theoretically. Eventually we fix on the notion of a structure in which the topology is “explicitly definable” in the sense of Flum and Ziegler [FZ]. In §2 we introduce the hypothesis that every definable set is a Boolean combination of definable open sets. In §3 we introduce a “dimension rank” on definable sets. In §4 we consider structures on which this rank is defined, and for which also every definable set has a finite number of definably connected definable components. We show that prime models over sets exist under such conditions. (shrink)

A topological constraint language is a formal language whose variables range over certain subsets of topological spaces, and whose nonlogical primitives are interpreted as topological relations and functions taking these subsets as arguments. Thus, topological constraint languages typically allow us to make assertions such as “region V1 touches the boundary of region V2”, “region V3 is connected” or “region V4 is a proper part of the closure of region V5”. A formula f in a topological constraint language is said to (...) be satisfiable if there exists an assignment to its variables of regions from some topological space under which φ is made true. This paper introduces a topological constraint language which, in addition to the usual mechanisms for expressing Boolean combinations of regions and their topological closures, includes primitives for bounding the number of components of a region. We call this language T CC, a rough acronym for “topological constraint language with component counting”. Our main result is that the problem of determining the satisfiability of a T CC-formula is NEXPTIME-complete. (shrink)

A structure (M, $ ,...) is called quasi-o-minimal if in any structure elementarily equivalent to it the definable subsets are exactly the Boolean combinations of 0-definable subsets and intervals. We give a series of natural examples of quasi-o-minimal structures which are not o-minimal; one of them is the ordered group of integers. We develop a technique to investigate quasi-o-minimality and use it to study quasi-o-minimal ordered groups (possibly with extra structure). Main results: any quasi-o-minimal ordered group is abelian; (...) any quasi-o-minimal ordered ring is a real closed field, or has zero multiplication; every quasi-o-minimal divisible ordered group is o-minimal; every quasi-o-minimal archimedian densely ordered group is divisible. We show that a counterpart of quasi-o-minimality in stability theory is the notion of theory of U-rank 1. (shrink)

We prove that S4 is complete with respect to Boolean combinations of countable unions of convex subsets of the real line, thus strengthening a 1944 result of McKinsey and Tarski 45 141). We also prove that the same result holds for the bimodal system S4+S5+C, which is a strengthening of a 1999 result of Shehtman 369).

We start with a nearly arbitrary standard classical first order "language" $C\sb{o},$ which is expanded to $C\sb{M,T}$ = "$C\sb{o}+M+T$", where for any variable x, M and T are unary formulas. We start also with a model ${\cal T}\sb{o},$ which together with $C\sb{o}$ represents a fixed non-problematic interpreted first order language. For each $\mu,\tau\subseteq U\sb{o},$ the universe of discourse for ${\cal T}\sb{o},$ the model ${\cal T}\sb{\mu,\tau}$ over $C\sb{M,T}$ is given so that its reduct to $C\sb{o}$ is just ${\cal T}\sb{o},$ and so (...) that for any $C\sb{M,T}$-variable x, the set-extensions of M and T are $\mu$ and $\tau$ respectively. For each $C\sb{M,T}$-expression e, $\vec e$ is its distinctly chosen representative in $U\sb{o},$ and $\lbrack\!\lbrack e\rbrack\!\rbrack$ is a constant $C\sb{o}$-term which names $\vec e.$ ;The goal is to find $\mu\sb*$ and $\tau\sb*,$ such that $\mu\sb*$ and $\tau\sb*$ plausibly and "self-referentially" approximate meaningfulness and truth respectively for any interpreted language represented by ${\cal T}\sb{\mu\sb*,\tau\sb*},$ by satisfying at least the following conditions. ; $\tau\sb*\subseteq\mu\sb*,$ and for each $C\sb{M,T}$-sentence $\sigma$ such that ${\cal T}\sb{\mu\sb*,\tau\sb*}\models M\lbrack\!\lbrack\sigma\rbrack\!\rbrack,$ $$\eqalign{&\ {\cal T}\sb{\mu\sb*,\tau\sb*} \models\sigma\Longleftrightarrow{\cal T}\sb{\mu\sb*,\tau\sb*}\models T\lbrack\!\lbrack\sigma\rbrack\!\rbrack,\ {\rm and}\cr&\ {\cal T}\sb{\mu\sb*,\tau\sb*}\models T\lbrack\!\lbrack\sigma\\leftrightarrow T\lbrack\!\lbrack\sigma\rbrack\!\rbrack\rbrack\!\rbrack.\cr}$$ ; There is a class of expression representatives $\mu\sp{D}\subseteq\mu\sb*$ containing every $C\sb{o}$-expression representative, such that the set $\tau\sp{D}=\mu\sp{D}\ \cap\ \tau\sb*$ itself satisfies the following properties. ;First, for each $\vec\sigma$ such that $\sigma$ is a $C\sb{M,T}$-sentence, if for all $\mu,\tau\subseteq U\sb{o}$ satisfying $\mu\supseteq\mu\sb*$ and $\tau\supseteq\tau\sp{D},$ it is the case that ${\cal T}\sb{\mu,\tau}\models\sigma,$ then $\vec\sigma\in\tau\sp{D}.$ ;Second, whenever $\vec\sigma\in\tau\sp{D},$ then also $\sp{\vec{\enspace}}\ \in\tau\sp{D}.$ ;Third, $\tau\sp{D}$ is "upwardly closed" with respect to the strong-Kleene rules for the truth-value evaluation of Boolean combinations of formulas. For example, for $C\sb{M,T}$-sentences $e\sb1$ and $e\sb2$: $$\eqalign{&\ \vec e\sb1\in\tau\sp{D}\Longleftrightarrow)\sp{\vec{\enspace}}\ \in\tau\sp{D}.\cr&\ {\rm If}\ \vec e\sb1\in\tau\sp{D}\ {\rm or}\ \vec e\sb2\in\tau\sp{D},\ {\rm then\ so\ is}\ \sp{\vec{\enspace}}\ \in\tau\sp{D}.\cr&\ {\rm If}\ \sp{\vec{\enspace}}\ \in\tau\sp{D}\ {\rm and}\ \sp{\vec{\enspace}}\ \in\tau\sp{D},\ {\rm then}\ )\sp{\vec{\enspace}}\ \in\tau\sp{D}.\cr}$$ ; For each $C\sb{M,T}$-expression e not involving T, ${\cal T}\sb{\mu\sb*,\tau\sb*}\models M\lbrack\!\lbrack e\rbrack\!\rbrack$; in particular, for any $C\sb{M,T}$-expression e whatsoever, ${\cal T}\sb{\mu\sb*,\tau\sb*}\models M\lbrack\!\lbrack\\neg M\lbrack\!\lbrack e\rbrack\!\rbrack\rbrack\!\rbrack.$ ; ;In this dissertation, it is shown for the first time that there are in fact $\mu\sb*$ and $\tau\sb*$ which simultaneously satisfy all three conditions , , and , even when the consequent of the Godel fixed point theorem must hold. (shrink)

We prove that: • if there is a model of I∆₀ + ¬ exp with cofinal Σ₁-definable elements and a Σ₁ truth definition for Σ₁ sentences, then I∆₀ + ¬ exp +¬BΣ₁ is consistent, • there is a model of I∆₀ Ω₁ + ¬ exp with cofinal Σ₁-definable elements, both a Σ₂ and a ∏₂ truth definition for Σ₁ sentences, and for each n > 2, a Σ n truth definition for Σ n sentences. The latter result is obtained by (...) constructing a model with a recursive truth-preserving translation of Σ₁ sentences into boolean combinations of $\exists \sum {\begin{array}{*{20}{c}} h \\ 0 \\ \end{array} } $ sentences. We also present an old but previously unpublished proof of the consistency of I∆₀ + ¬ exp + ¬BΣ₁ under the assumption that the size parameter in Lessan's ∆₀ universal formula is optimal. We then discuss a possible reason why proving the consistency of I∆₀ + ¬ exp + ¬BΣ₁ unconditionally has turned out to be so difficult. (shrink)

Causal Modeling Semantics (CMS, e.g., Galles and Pearl 1998; Pearl 2000; Halpern 2000) is a powerful framework for evaluating counterfactuals whose antecedent is a conjunction of atomic formulas. We extend CMS to an evaluation of the probability of counterfactuals with disjunctive antecedents, and more generally, to counterfactuals whose antecedent is an arbitrary Boolean combination of atomic formulas. Our main idea is to assign a probability to a counterfactual (A ∨ B) > C at a causal model M as a (...) weighted average of the probability of C in those submodels that truthmake A∨ B (Briggs 2012; Fine 2016, 2017). The weights of the submodels are given by the inverse distance to the original model M, based on a distance metric proposed by Eva, Stern, and Hartmann (2019). Apart from solving a major problem in the epistemology of counterfactuals, our paper shows how work in semantics, causal inference and formal epistemology can be fruitfully combined. (shrink)

We show that given a finite, transitive and reflexive Kripke model 〈 W , ≼, ⟦ ⋅ ⟧ 〉 and $${w \in W}$$ , the property of being simulated by w (i.e., lying on the image of a literalpreserving relation satisfying the ‘forth’ condition of bisimulation) is modally undefinable within the class of S4 Kripke models. Note the contrast to the fact that lying in the image of w under a bi simulation is definable in the standard modal language even (...) over the class of K4 models, a fairly standard result for which we also provide a proof. We then propose a minor extension of the language adding a sequent operator $${\natural}$$ (‘tangle’) which can be interpreted over Kripke models as well as over topological spaces. Over finite Kripke models it indicates the existence of clusters satisfying a specified set of formulas, very similar to an operator introduced by Dawar and Otto. In the extended language $${{\sf L}^+ = {\sf L}^{\square\natural}}$$ , being simulated by a point on a finite transitive Kripke model becomes definable, both over the class of (arbitrary) Kripke models and over the class of topological S4 models. As a consequence of this we obtain the result that any class of finite, transitive models over finitely many propositional variables which is closed under simulability is also definable in L + , as well as Boolean combinations of these classes. From this it follows that the μ -calculus interpreted over any such class of models is decidable. (shrink)

One of central problems in the theory of conditionals is the construction of a probability space, where conditionals can be interpreted as events and assigned probabilities. The problem has been given a technical formulation by van Fraassen (23), who also discussed in great detail the solution in the form of Stalnaker Bernoulli spaces. These spaces are very complex – they have the cardinality of the continuum, even if the language is finite. A natural question is, therefore, whether a technically simpler (...) (in particular finite) partial construction can be given. In the paper we provide a new solution to the problem. We show how to construct a finite probability space $$\mathrm {S}^\#=\left(\mathrm\Omega^\#,\mathrm\Sigma^\#,\mathrm P^\#\right)$$ S # = Ω #, Σ #, P # in which simple conditionals and their Boolean combinations can be interpreted. The structure is minimal in terms of cardinality within a certain, naturally defined class of models – an interesting side-effect is an estimate of the number of non-equivalent propositions in the conditional language. We demand that the structure satisfy certain natural assumptions concerning the logic and semantics of conditionals and also that it satisfy PCCP. The construction can be easily iterated, producing interpretations for conditionals of arbitrary complexity. (shrink)

This paper presents a generalization of the standard notions of left monotonicity (on the nominal argument of a determiner) and right monotonicity (on the VP argument of a determiner). Determiners such as “more than/at least as many as” or “fewer than/at most as many as”, which occur in so-called propositional comparison, are shown to be monotone with respect to two nominal arguments and two VP-arguments. In addition, it is argued that the standard Generalized Quantifier analysis of numerical determiners such as (...) “more than three/at least three” is a simplification which ignores the fundamental parallellism with the propositional comparatives. Furthermore, the symmetric monotonicity configurations of the existential “some” and “no” are shown to be straightforwardly related to those of numerical comparatives with the limit numeral zero, whereas the asymmetric configurations of universal “all” and “not all” involve the extra complicating mechanism of polarity reversal, which is related to Keenan's notion of co-intersectivity (as opposed to intersectivity). A second aim of the paper is to investigate some of the factors reducing the inferential potential of determiners. Different types of comparative determiners and their modification will be considered in detail. In addition, a systematic interaction will be revealed between the monotonicity properties of the determiners in propositional comparatives and the differ ent types of ellipsis in the “than”-complement. Different degrees of ellipsis are defined in terms of informational dependencies between the “than”-complement and the main clause. A general balancing mechanism is observed by virtue of which an increase in informational dependency is compensated by a reduction of the inferential potential of the comparative determiner. The structure of the paper is as follows. Part two deals with propositional comparison and introduces the two basic monotonicity configurations. Part three distinguishes three types of informational dependencies or ellipsis between the “than”-complement and the main clause. In Section 3.1 the “than”-complement only contains a VP constituent, whereas in Section 3.2. it only consists of a nominal constituent. Section 3.3 considers more complex instances of multiple dependencies. Section 3.4 then looks at the interaction of these three types with the modifier “proportionally”. Part four presents the two basic monotonicity configurations for numerical comparison, whereas part five deals with more complex numerical determiners. Bounding determiners, such as “between five and ten”, and other boolean combinations are discussed in Section 5.1, whereas Section 5.2 goes into approximative determiners involving modifiers such as “only” or “almost”. Section 5.3. is devoted to proportional determiners such as “more than two out of three”. Part six then considers the standard existential and universal quantifiers. Section 6.1 reformulates the standard Generalized Quantifier analysis in comparative terms, whereas Section 6.2 deals with exception determiners of the form “all but five”. (shrink)

A first-order theory is equational if every definable set is a Boolean combination of instances of equations, that is, of formulae such that the family of finite intersections of instances has the descending chain condition. Equationality is a strengthening of stability. We show the equationality of the theory of proper extensions of algebraically closed fields and of the theory of separably closed fields of arbitrary imperfection degree.

We prove that if M is any model of a trivial, weakly minimal theory, then the elementary diagram T(M) eliminates quantifiers down to Boolean combinations of certain existential formulas.

We present a canonical form for definable subsets of algebraically closed valued fields by means of decompositions into sets of a simple form, and do the same for definable subsets of real closed valued fields. Both cases involve discs, forming "Swiss cheeses" in the algebraically closed case, and cuts in the real closed case. As a step in the development, we give a proof for the fact that in "most" valued fields F, if f(x),g(x) ∈ F[ x] and v is (...) the valuation map, then the set {x : v(f(x)) ≤ v(g(x))} is a Boolean combination of discs; in fact, it is a finite union of Swiss cheeses. The development also depends on the introduction of "valued trees", which we define formally. (shrink)

Formulas of the propositional modal language with the unary modal operators □, Σ1, 1, Σ2, 2,… are considered as schemata of sentences of arithmetic , where □A is interpreted as “A is PA-provable”, ΣnA as “A is PA-equivalent to a Σn-sentence” and nA as “A is PA-equivalent to a Boolean combination of Σn-sentences”. We give an axiomatization and show decidability of the sets of the modal formulas which are schemata of: PA-provable, true arithmetical sentences.

In this paper the PA-completeness of modal logic is studied by syntactical and constructive methods. The main results are theorems on the structure of the PA-proofs of suitable arithmetical interpretationsS of a modal sequentS, which allow the transformation of PA-proofs ofS into proof-trees similar to modal proof-trees. As an application of such theorems, a proof of Solovay's theorem on arithmetical completeness of the modal system G is presented for the class of modal sequents of Boolean combinations of formulas (...) of the form p i,m i=0, 1, 2, ... The paper is the preliminary step for a forthcoming global syntactical resolution of the PA-completeness problem for modal logic. (shrink)

Several attempts have been done to distinguish “positive” information in an arbitrary first order theory, i.e., to find a well behaved class of closed sets among the definable sets. In many cases, a definable set is said to be closed if its conjugates are sufficiently distinct from each other. Each such definition yields a class of theories, namely those where all definable sets are constructible, i.e., boolean combinations of closed sets. Here are some examples, ordered by strength:Weak normality (...) describes a rather small class of theories which are well understood by now (see, for example, [P]). On the other hand, normalization is so weak that all theories, in a suitable context, are normalizable (see [HH]). Thus equational theories form an interesting intermediate class of theories. Little work has been done so far. The original work of Srour [S1, S2, S3] adopts a point of view that is closer to universal algebra than to stability theory. The fundamental definitions and model theoretic properties can be found in [PS], though some easy observations are missing there. Hrushovski's example of a stable non-equational theory, the first and only one so far, is described in the unfortunately unpublished manuscript [HS]. In fact, it is an expansion of the free pseudospace constructed independently by Baudisch and Pillay in [BP] as an example of a strictly 2-ample theory. Strong equationality, defined in [Hr], is also investigated in [HS]. (shrink)

We start with a simple proof of Leivant's normal form theorem for ∑11 formulas over finite successor structures. Then we use that normal form to prove the following:1. over all finite structures, every ∑21 formula is equivalent to a ∑21 formula whose first-order part is a Boolean combination of existential formulas, and2. over finite successor structures, the Kolaitis-Thakur hierarchy of minimization problems collapses completely and the Kolaitis-Thakur hierarchy of maximization problems collapses partially.The normal form theorem for ∑21 fails if (...) ∑21 is replaced with ∑11 or if infinite structures are allowed. (shrink)

We consider games over a finite alphabet with Gurevich-Harrington's winning conditions and restraints as in Yakhnis-Yakhnis . The game tree, the Gurevich-Harrington's kernels of the winning condition and the restraints are defined by finite automata. We give an effective criterion to determine the winning player and an effective presentation of a class of finite automata defined winning strategies.Our approach yields an alternative solution to the games considered by Büchi and Landweber . The BL algorithm is an important tool for solving (...) effectively presented games. The differences between the BL and our algorithms are as follows. Our algorithm is uniformly applicable to winning sets that correspond to boolean combinations of BL winning conditions, while the BL algorithm requires a transformation of such boolean combinations into a single BL condition. Our algorithm directly applies to a larger class of game trees for a given game alphabet than does the BL one. We describe Büchi-Landweber's class of winning conditions in a more transparent way by using finite automata and Gurevich-Harrington's form of winning conditions. Our algorithms that determine the winner of the game and find a winning strategy, are based on a translation of the events in the game in terms of the transition table of the automaton representing the game. This automaton differs from the ones that represent BL winning conditions. Both algorithms need further investigation.The algorithm determining the winner in the game, can be used as a verifier of concurrent programs. This is because programs can be viewed as strategies in Gurevich-Harrington's games and program specifications could be regarded as winning conditions for such games. The algorithm which finds a winning strategy could be used as a basis for automated concurrent program design.The present paper is a sequel to Annals of Pure and Applied Logic 48 277–297. (shrink)

The aim of this paper is to give new kinds of modal logics suitable for reasoning about regions in discrete spaces. We call them dynamic logics of the region-based theory of discrete spaces. These modal logics are linguistic restrictions of propositional dynamic logic with the global diamond E. Their formulas are equivalent to Boolean combinations of modal formulas like E(A ∧ ⟨α⟩ B) where A and B are Boolean terms and α is a relational term. Examining what (...) we can say about dynamic models when we use formulas to describe them, we successively address the axiomatization/completeness issue and the decidability/complexity issue of our dynamic logics of the region-based theory of discrete spaces. (shrink)

Each closed (i.e. variable free) formula of interpretability logic is equivalent in ILF to a closed formula of the provability logic G, thus to a Boolean combination of formulas of the form n.

Jamie Dreier has argued that the supervenience of the moral on the non-moral requires explanation, and that attempts by the non-naturalist to provide it, or to sidestep the issue, have so far failed. These comments on Dreier first examine the notion of distinctness at work in the idea that non-natural properties are distinct from natural ones, pointing out that distinctness cannot be understood in modal terms if supervenience is to be respected. It then suggests that Dreier’s implicit commitment to the (...) existence of infinite Boolean combinations of properties plays a significant role in the challenge to non-naturalism, and that the non-naturalist has some principled reasons for rejecting it. It also suggests that the real problem for non-naturalists isn’t explaining supervenience, but is rather the well-known problem of explaining our capacity to know anything about non-natural properties. That is, if the latter epistemological problem can be solved, the former metaphysical one might well disappear, at least as a distinctive problem for non-naturalist realists about morality. (shrink)

We introduce the notion of "semi-r.e." for subsets of ω, a generalization of "semirecursive" and of "r.e.", and the notion of "weakly semirecursive", a generalization of "semi-r.e.". We show that A is weakly semirecursive iff, for any n numbers x 1 ,...,x n , knowing how many of these numbers belong to A is equivalent to knowing which of these numbers belong to A. It is shown that there exist weakly semirecursive sets that are neither semi-r.e. nor co-semi-r.e. On the (...) other hand, we exhibit nonzero Turing degrees in which every weakly semirecursive set is semirecursive. We characterize the notion "A is weakly semirecursive and recursive in K" in terms of recursive approximations to A. We also show that if a finite Boolean combination of r.e. sets is semirecursive then it must be r.e. or co-r.e. Several open questions are raised. (shrink)

This paper looks at the concept of neighborhood canonicity introduced by BRIAN CHELLAS [2]. We follow the lead of the author's paper [9] where it was shown that every non-iterative logic is neighborhood canonical and here we will show that all logics whose axioms have a simple syntactic form-no intensional operator is in boolean combination with a propositional letter-and which have the finite model property are neighborhood canonical. One consequence of this is that KMcK, the McKinsey logic, is neighborhood (...) canonical, an interesting counterpoint to the results of ROBERT GOLDBLATT and XIAOPING WANG who showed, respectively, that KMcK is not relational canonical [5] and that KMcK is not relationally strongly complete [11]. (shrink)

It was recently shown that the theories of generic algebraic curves converge to a limit theory as their degrees go to infinity. In this paper we give quantitative versions of this result and other similar results. In particular, we show that generic curves of degree higher than 22r cannot be distinguished by a first-order formula of quantifier rank r. A decision algorithm for the limit theory then follows easily. We also show that in this theory all formulas are equivalent to (...) boolean combinations of existential formulas, and give a quantitative version of this result. (shrink)

A conception of an information system has been introduced by Pawlak. The study has been continued in works of Pawlak and Orlowska and in works of Vakarelov. They had proposed some basic relations and had constructed a formal system of a modal logic that describes the relations and some of their Boolean combinations. Our work is devoted to a generalization of this approach. A class of relation systems and a complete calculus construction method for these systems are proposed. (...) As a corollary of our main result, our paper contains a solution of a Vakarelov's problem: how to construct a formal system that describes all the Boolean combinations of the basic relations. (shrink)

We prove (in ZFC Set Theory) that all infinite games whose winning sets are of the following forms are determined: (1) (A - S) ∪ B, where A is $\Pi^0_2, \bar\bar{S}, 2^{\aleph_0}$ , and the games whose winning set is B is "strongly determined" (meaning that all of its subgames are determined). (2) A Boolean combination of Σ 0 2 sets and sets smaller than the continuum. This also enables us to show that strong determinateness is not preserved under (...) complementation, improving a result of Morton Davis which required the continuum hypothesis to prove this fact. Various open questions related to the above results are discussed. Our main conjecture is that (2) above remains true when "Σ 0 2 " is replaced by "Borel". (shrink)

Coalgebras of polynomial functors constructed from sets of observable elements have been found useful in modelling various kinds of data types and state-transition systems. This paper continues the study of equational logic and model theory for polynomial coalgebras begun in Goldblatt , where it was shown that Boolean combinations of equations between terms of observable type form a natural language of observable formulas for specifying properties of polynomial coalgebras, and for giving a Hennessy–Milner style logical characterisation of observational (...) indistinguishability of states.Here we give a structural characterisation of classes of coalgebras definable by observable formulas. This is an analogue for polynomial coalgebras of Birkhoff's celebrated characterisation of equationally definable classes of abstract algebras as being those closed under homomorphic images, subalgebras, and direct products. The coalgebraic characterisation involves new notions of observational ultraproduct and ultrapower of coalgebras, obtained from the classical construction of ultraproducts by deleting states that assign “nonstandard” values to terms of observable type. A class of polynomial coalgebras is shown to be the class of all models of a set of observable formulas if, and only if, it is closed under images of bisimulation relations, disjoint unions and observational ultrapowers.Observational ultraproducts are also used to discuss compactness—which holds only under limited conditions; to characterise finitely, axiomatisable classes of polynomial coalgebras; and to show that there are axiomatisable classes that are not finitely axiomatisable. (shrink)

Linear temporal logic with Since and Until modalities is expressively equivalent, over the class of complete linear orders, to a fragment of first-order logic known as FOMLO. It turns out that LTL, under some basic assumptions, is expressively complete if and only if it has the property, called separation, that every formula is equivalent to a Boolean combination of formulas that each refer only to the past, present or future. Herein we present simple algorithms and their implementations to perform (...) separation of the LTL with Since and Until, over discrete and complete linear orders, and translation from FOMLO formulas into equivalent temporal logic formulas. We additionally show that the separation of a certain fragment of LTL results in at most a double exponential size growth. (shrink)