The strong order property 1 (SOP _1 ) is a model-theoretic tree property introduced by Džamonja and Shelah. We give an exposition of a family of results around NSOP _1 theories, explaining why the NSOP _1 /SOP _1 divide is a meaningful dividing line among first-order theories. This involves summarizing work on Kim-independence and on the interpretability order, as well as aspects of Mutchnik’s work on SOP _1 and SOP _2 .
We propose and investigate a new model of a distributed game played on a non-deterministic asynchronous transition system over two processes. This game is played between an environment and a distributed team of the two processes where each process has only partial information of the ongoing play – namely complete information up to the last synchronization and only its own local evolution since this last synchronization. The key algorithmic decision problem, for a given winning objective, is the existence of a distributed co-operative winning strategy for the team to meet that objective. We address this question for global safety, local reachability and global/simultaneous reachability objectives. We carry out a thorough analysis of these games and present natural fixpoint based algorithms for solving them. This allows us to construct distributed winning strategies with an explicit distributed finite-memory in the form of key past information, and also yields near optimal decision procedures. Specifically, our analysis shows that the decision problems for global safety and local reachability objectives are NP-complete. We also establish that the decision problem for global reachability objective is PSPACE-hard and provide an NEXPTIME algorithm for the same.
Over forty years ago, E.P. Specker and C. Blatter discovered an astonishing meta-theorem about combinatorial counting functions definable in Monadic Second Order Logic (MSOL). In this talk we discuss extensions and limit of this theorem and its wide-ranging applications.
This article introduces a new semantics for the basic modal language, motivated by rough set theory. Additionally, a sound and complete deductive system relative to two important classes of models are obtained.
In this paper, we establish the Craig interpolation theorems of awareness logics by introducing semi-analytic sequent calculi for them. For a semantic clause for an awareness operator, we choose an idea of propositional awareness, which is introduced by Fagin and Halpern and means that an agent is aware of a formula if and only if he is aware of all the atomic propositions contained in it. Although our sequent calculi are not cut-free (due to the fact that our epistemic logic is based on S5), we are able to restrict all applications of the rule of cut to semi-analytic ones. This enables us to employ the Maehara method in order to compute Craig interpolants.
Arbitrary Public Announcement Logic (APAL) and its variants are proposed to formalize knowability dynamically based on public announcements as the means to update knowledge. In this paper, we introduce yet another variant HAPAL of APAL, which is based on questions instead of announcements, and captures knowability as knowing how to know by asking questions. Therefore, the prime modality in our language can also be viewed as a know-how operator sharing the same ∃ bundled structure as logics of knowing how in the literature. This change in the semantics of the arbitrary announcement operator results in a highly non-trivial logic, which departs from the existing versions of APAL. As we will show, it is already strictly more expressive than APAL and epistemic logic on S5 models in the single-agent case. Moreover, it lacks compactness and Craig interpolation property. We also provide a sound and weakly complete axiomatization.
Mīmāṃsā, one of the systems of Indian Philosophy, deals with the interpretation of the Vedas. The Brāhmaṅas, a division of the Vedas, include precise instructions (Vidhi) for the execution of rituals. Interpreting these immediately can be confusing. In order to fully understand this, the interpretive processes from Mīmāṃsā are utilized. The procedures encompass various components, such as linguistic proficiency, grammatical comprehension, the individual’s capacity to execute the ritual, and logical attributes. In addition, Mīmāṃsā incorporates a mention of diverse sequencing systems known as krama, which precisely outlines the specified sequence in which rituals should be performed. This paper takes inspiration from these sequential techniques and proposes a framework for temporal reasoning from a Logical perspective. This approach is incorporated into the existing MIRA (Mīmāṃsā Inspired Representation of Actions) work, resulting in activity sequencing. Subsequently, it is utilized in the Large Language Models to autonomously produce a sequence of instructions in real-life situations.
In this paper, we propose a new version of complete logic—Ŀogic of İnexact K̇nowledge ( )—that has the following eight features out of which the seven can reflect Williamson (1994)’s arguments but out of which the only one is essentially different from the features based on Williamson’s knowledge first epistemology: 1. This model based on additively-semiordered qualitative conditional probability that is a qualitatively-probabilistic counterpart of a JND which is a psychophysical counterpart of a margin for error can reflect the essence of inexact knowledge. 2. We can formalize a margin for error principle in . 3. The width of a margin for error (JND) depends on the cognitive capacities. 4. In , the direct indiscriminability relation is a non-transitive relation. 5. The reason why we introduce qualitative not absolute but conditional probability is to make it possible to express the direct indiscriminability between the two events on the condition that either of the two occurs. 6. has so rich expressive power as to fully formalize such inferences as (6)–(8). 7. The KK principle is not valid in . 8. Essential Difference: In Williamson’s inexact knowledge is primitive based on his knowledge first epistemology, whereas in inexact knowledge is defined in terms of the direct indiscriminability relation based on our direct indiscriminability relation first epistemology.
In logic, quantifiers typically have an implicit linear order of dependencies. Henkin introduced a more general framework for quantifier prefixes, allowing for partial orderings among quantifiers. These quantifiers, now known as Henkin quantifiers, have been extensively studied in logic and have found significant applications in linguistics, arithmetic, and descriptive complexity. Surprisingly, bounded versions of Henkin quantifiers, which restrict the range of these quantifiers, have not been explored. This paper defines bounded Henkin quantifiers and examines their properties from a complexity-theoretic perspective. In particular, we show that the set of predicates definable by quantifier-free formulas prefixed by a bounded Henkin quantifier is exactly . The proof goes via machine models defined using bounded Henkin quantifiers. Finally, we show that formulas with Henkin quantifiers define a complexity class contained in _2 in the exponential hierarchy and define a natural complete problem for this class.
In this paper, based on duality-theoretic techniques, we introduce a sound and complete neighborhood semantics based on polarities for basic lattice-based monotone modal logic, and show that monotone modal operators in lattice-based monotone modal logic can be represented as the composition of suitable normal modal operators via a multi-type representation of complete lattices with monotone operators.
We consider the class of finite spiked Boolean algebras introduced by Inamdar and show that the modal and intermediate logics associated to it are not finitely axiomatisable.
In this paper, we present an algebra-valued model on top of the four-element lattice 𝕄ℂ which semantically captures Wansing’s logic of material connexvity (MC). We show that the resulting model validates an axiom system that is classically equivalent to . For this purpose, we tweak our semantic interpretation of set-membership and identity.
This work addresses the problem of synthesizing fuzzy temporal logic rules from a set of given positive and negative examples. The examples are provided in the form of execution traces of finite length. Fuzzy Time Linear Temporal Logic over finite traces (FTLf) is chosen as the language for rule synthesis. FTLf is capable of capturing fuzzy temporal modalities, like, 'soon after', 'almost always', 'gradually' etc., that make the learnt rules simpler and more understandable than classical LTL representations. The proposed approach reduces the learning task to a multi-valued partial maximum satisfiability (PMaxSAT) problem. This work is useful for generating interpretable explanations of complex system behaviours.
Logic in Computer Science plays important roles ranging from formal methods to Human-Computer Interaction, including Software and Hardware Engineering, etc. Regarding the former broad application domain of formal methods, a tremendous amount of work concern verification, namely satisfiability checking (for model synthesis) and model checking (for counterexample/witness synthesis). I want to discuss a fairly novel question, called Formula Synthesis Problem, that I believe is extremely natural to address, and yet has not received enough attention in logic. In its most general form, the Formula Synthesis Problem consists in deciding whether some formula in a given set is satisfied by a given model (and output one if any). Obviously, if the input set of formulas is finite, this amounts to model checking. On the contrary, if this set is infinite, say obtained by some tree-grammar for formulas, then the answer becomes extraordinary challenging. As far as I am aware of, only in [17], the authors (part of which I am) have addressed the problem for the first time, in the particular case of the logic Propositional Dynamic Logic (PDL) extended with shuffle ( PDL^|| ), a deeply-studied logic in the literature. The obtained results regarding this instance of the Formula Synthesis Problem, called synthPDL^|| , were published in a strongly AI-tainted conference, since it is AAAI 2022. I wish hereby to let these results be known by a broader audience, and in particular by the community of logic and formal methods. This, all the more than the contribution on synthPDL^|| opens up connections to other problems in other Computer Science fields such as planning and security.
The use of monoids in the study of word languages recognized by finite-state automata has been quite fruitful. In this work, we look at the same idea of "recognizability by finite monoids" for other monoids. In particular, we attempt to characterize recognizable subsets of various additive and multiplicative monoids over integers, rationals, reals, and complex numbers. While these recognizable sets satisfy properties such as closure under Boolean operations and inverse morphisms, they do not enjoy many of the nice properties that recognizable word languages do.
This paper introduces deterministic weighted real-time one-counter automaton (dwroca). A dwroca is a deterministic real-time one-counter automaton whose transitions are assigned a weight from a field. Two dwrocas are equivalent if every word accepted by one is accepted by the other with the same weight. dwroca is a sub-class of weighted one-counter automata with counter-determinacy. It is known that the equivalence problem for this model is in [7]. This paper gives a simpler proof and a better polynomial-time algorithm for checking the equivalence of two dwrocas.
The variable inclusion companions of logics have lately been thoroughly studied by multiple authors. There are broadly two types of these companions: the left and the right variable inclusion companions. Another type of companions of logics induced by Hilbert-style presentations (Hilbert-style logics) were introduced in [1]. A sufficient condition for the restricted rules companion of a Hilbert-style logic to coincide with its left variable inclusion companion was proved there, while a necessary condition remained elusive. The present article has two parts. In the first part, we give a necessary and sufficient condition for the left variable inclusion and the restricted rules companions of a Hilbert-style logic to coincide. In the rest of the paper, we recognize that the variable inclusion restrictions used to define variable inclusion companions of a logic ⟨ℒ,⊢⟩ are relations from 𝒫(ℒ) to ℒ . This leads to a more general idea of a relational companion of a logical structure, a framework that we borrow from the field of universal logic. We end by showing that even Hilbert-style logics and the restricted rules companions of these can be brought under the umbrella of the general notions of logical structures and their relational companions that are discussed here.
Abstract In this paper we study a notion of HL-extension (HL standing for Herwig–Lascar) for a structure in a finite relational language $\mathcal {L}$ . We give a description of all finite minimal HL-extensions of a given finite $\mathcal {L}$ -structure. In addition, we study a group-theoretic property considered by Herwig–Lascar and show that it is closed under taking free products. We also introduce notions of coherent extensions and ultraextensive $\mathcal {L}$ -structures and show that every countable $\mathcal {L}$ -structure can be extended to a countable ultraextensive structure. Finally, it follows from our results that the automorphism group of any countable ultraextensive $\mathcal {L}$ -structure has a dense locally finite subgroup.
This work introduces modal logics for varieties of normal topological quasi-Boolean algebras. Relational semantics for these modal logics using involutive frames are established. A discrete duality is given for involutive frames and normal topological quasi-Boolean algebras. Some results on Kripke-completeness and finite model property are given.
For each non-zero cardinal $$\kappa $$ , we introduce a generalized separation axiom $$T_0^\kappa $$ for topological spaces. For every integer $$n>0$$ , under the $$\textsf{d}$$ -semantics which interpret $$\Diamond $$ as the derived set operator in a topological space, the class of all $$T_0^{n}$$ -spaces is $$\textsf{d}$$ -defined by the modal formula $$\textrm{t}_0^n$$ , and we show that $$\textsf{wK4T}_0^n=\textsf{wK4}\oplus \textrm{t}_0^n$$ is the $$\textsf{d}$$ -logic of all $$T_0^n$$ -spaces. For $$\kappa \ge \aleph _0$$ , the class of all $$T_0^\kappa $$ -spaces is not $$\textsf{d}$$ -definable.
