On the Presburger fragment of logics with multiteam semantics

In team semantics, which is the basis of modern logics of dependence and independence, formulae are evaluated on sets of assignments, called teams. Multiteam semantics instead takes mulitplicities of data into account and is based on multisets of assignments, called multiteams. Logics with multiteam semantics can be embedded into a two-sorted variant of existential second-order logics, with arithmetic operations on multiplicities. Here we study the Presburger fragment of such logics, permitting only addition, but not multiplication on multiplicities. It can be shown that this fragment corresponds to inclusion-exclusion logic in multiteam semantics, but, in contrast to the situation in team semantics, that it is strictly contained in independence logic. We give different characterisations of this fragment by various atomic dependency notions.     

Tractability frontiers in probabilistic team semantics and existential second-order logic over the reals

Probabilistic team semantics is a framework for logical analysis of probabilistic dependencies. Our focus is on the axiomatizability, complexity, and expressivity of probabilistic inclusion logic and its extensions. We identify a natural fragment of existential second-order logic with additive real arithmetic that captures exactly the expressivity of probabilistic inclusion logic. We furthermore relate these formalisms to linear programming, and doing so obtain PTIME data complexity for the logics. Moreover, on finite structures, we show that the full existential second-order logic with additive real arithmetic can only express NP properties. Lastly, we present a sound and complete axiomatization for probabilistic inclusion logic at the atomic level.     

On elementary logics for quantitative dependencies

We define and study logics in the framework of probabilistic team semantics and over metafinite structures. Our work is paralleled by the recent development of novel axiomatizable and tractable logics in team semantics that are closed under the Boolean negation. Our logics employ new probabilistic atoms that resemble so-called extended atoms from the team semantics literature. We also define counterparts of our logics over metafinite structures and show that all of our logics can be translated into functional fixed point logic implying a polynomial time upper bound for data complexity with respect to BSS-computations.     

On intermediate inquisitive and dependence logics: An algebraic study

This article provides an algebraic study of intermediate inquisitive and dependence logics. While these logics are usually investigated using team semantics, here we introduce an alternative algebraic semantics and we prove it is complete for all intermediate inquisitive and dependence logics. To this end, we define inquisitive and dependence algebras and we investigate their model-theoretic properties. We then focus on finite, core-generated, well-connected inquisitive and dependence algebras: we show they witness the validity of formulas true in inquisitive algebras, and of formulas true in well-connected dependence algebras. Finally, we obtain representation theorems for finite, core-generated, well-connected, inquisitive and dependence algebras and we prove some results connecting team and algebraic semantics.     

Some Connections between Topological and Modal Logic

We study modal logics based on neighbourhood semantics using methods and theorems having their origin in topological model theory. We thus obtain general results concerning completeness of modal logics based on neighbourhood semantics as well as the relationship between neighbourhood and Kripke semantics. We also give a new proof for a known interpolation result of modal logic using an interpolation theorem of topological model theory.     

A Sahlqvist theorem for distributive modal logic

In this paper we consider distributive modal logic, a setting in which we may add modalities, such as classical types of modalities as well as weak forms of negation, to the fragment of classical propositional logic given by conjunction, disjunction, true, and false. For these logics we define both algebraic semantics, in the form of distributive modal algebras, and relational semantics, in the form of ordered Kripke structures. The main contributions of this paper lie in extending the notion of Sahlqvist axioms to our generalized setting and proving both a correspondence and a canonicity result for distributive modal logics axiomatized by Sahlqvist axioms. Our proof of the correspondence result relies on a reduction to the classical case, but our canonicity proof departs from the traditional style and uses the newly extended algebraic theory of canonical extensions.     

A probabilistic logic based on the acceptability of gambles

This article presents a probabilistic logic whose sentences can be interpreted as asserting the acceptability of gambles described in terms of an underlying logic. This probabilistic logic has a concrete syntax and a complete inference procedure, and it handles conditional as well as unconditional probabilities. It synthesizes Nilsson’s probabilistic logic and Frisch and Haddawy’s anytime inference procedure with Wilson and Moral’s logic of gambles.Two distinct semantics can be used for our probabilistic logic: (1) the measure–theoretic semantics used by the prior logics already mentioned and also by the more expressive logic of Fagin, Halpern, and Meggido and (2) a behavioral semantics. Under the measure–theoretic semantics, sentences of our probabilistic logic are interpreted as assertions about a probability distribution over interpretations of the underlying logic. Under the behavioral semantics, these sentences are interpreted only as asserting the acceptability of gambles, and this suggests different directions for generalization.     

Fibered universal algebra for first-order logics

We extend Lawvere-Pitts prop-categories (aka. hyperdoctrines) to develop a general framework for providing fibered algebraic semantics for general first-order logics. This framework includes a natural notion of substitution, which allows first-order logics to be considered as structural closure operators just as propositional logics are in abstract algebraic logic. We then establish an extension of the homomorphism theorem from universal algebra for generalized prop-categories and characterize two natural closure operators on the prop-categorical semantics. The first closes a class of structures (which are interpreted as morphisms of prop-categories) under the satisfaction of their common first-order theory and the second closes a class of prop-categories under their associated first-order consequence. It turns out that these closure operators have characterizations that closely mirror Birkhoff's characterization of the closure of a class of algebras under the satisfaction of their common equational theory and Blok and Jónsson's characterization of closure under equational consequence, respectively. These algebraic characterizations of the first-order closure operators are unique to the prop-categorical semantics. They do not have analogues, for example, in the Tarskian semantics for classical first-order logic. The prop-categories we consider are much more general than traditional intuitionistic prop-categories or triposes (i.e., topos representing indexed partially ordered sets). Nonetheless, to the best of our knowledge, our results are new, even when restricted to these special classes of prop-categories.     

A Universal Logic Approach to Adaptive Logics

In this paper, adaptive logics are studied from the viewpoint of universal logic (in the sense of the study of common structures of logics). The common structure of a large set of adaptive logics is described. It is shown that this structure determines the proof theory as well as the semantics of the adaptive logics, and moreover that most properties of the logics can be proved by relying solely on the structure, viz. without invoking any specific properties of the logics themselves.     

Formal similarities and differences among qualitative conditional semantics

Various semantics have been used for conditionals in the area of knowledge representation and reasoning. In this paper, we study similarities and differences between a purely qualitative semantics based on the popular system-of-spheres semantics of Lewis, an ordinal semantics making use of rankings, a possibilistic semantics, and a semantics representing conditionals by probabilities in a qualitative way. As a common framework for the corresponding logics, we use Goguen and Burstall’s notion of institutions whose central motto is that truth is invariant under the change of notation. The institution framework provides the formal rigidity needed for our investigation, but leaves enough abstract freedom to formalize and compare quite different logics. We show precisely in which sense the conditional semantics mentioned above are logically similar, and point out the semantical subtleties each semantics allows.     

Infinitary S5-Epistemic Logic

It is known that a theory in S5-epistemic logic with several agents may have numerous models. This is because each such model specifies also what an agent knows about infinite intersections of events, while the expressive power of the logic is limited to finite conjunctions of formulas. We show that this asymmetry between syntax and semantics persists also when infinite conjunctions (up to some given cardinality) are permitted in the language. We develop a strengthened S5-axiomatic system for such infinitary logics, and prove a strong completeness theorem for them. Then we show that in every such logic there is always a theory with more than one model.     

Propositional union closed team logics

In this paper, we study several propositional team logics that are closed under unions, including propositional inclusion logic. We show that all these logics are expressively complete, and we introduce sound and complete systems of natural deduction for these logics. We also discuss the locality property and its connection with interpolation in these logics.     

Structuring Co-constructive Logic for Proofs and Refutations

This paper considers a topos-theoretic structure for the interpretation of co-constructive logic for proofs and refutations following Trafford (Studia Humana 3(4):22–40, 2015). It is notoriously tricky to define a proof-theoretic semantics for logics that adequately represent constructivity over proofs and refutations. By developing abstractions of elementary topoi, we consider an elementary topos as structure for proofs, and complement topos as structure for refutation. In doing so, it is possible to consider a dialogue structure between these topoi, and also control their relation such that classical logic (interpreted in a Boolean topos) is simulated where proofs and refutations are conclusive.     

Relating and extending semantical approaches to possibilistic reasoning

Two main semantical approaches to possibilistic reasoning with classical propositions have been proposed in the literature. Namely, Dubois-Prade's approach known as possibilistic logic, whose semantics is based on a preference ordering in the set of possible worlds, and Ruspini's approach that we redefine and call similarity logic, which relies on the notion of similarity or resemblance between worlds. In this article we put into relation both approaches, and it is shown that the monotonic fragment of possibilistic logic can be semantically embedded into similarity logic. Furthermore, to extend possibilistic reasoning to deal with fuzzy propositions, a semantical reasoning framework, called fuzzy truth-valued logic, is also introduced and proved to capture the semantics of both possibilistic and similarity logics.     

Unifying hidden-variable problems from quantum mechanics by logics of dependence and independence

We study hidden-variable models from quantum mechanics and their abstractions in purely probabilistic and relational frameworks by means of logics of dependence and independence, which are based on team semantics. We show that common desirable properties of hidden-variable models can be defined in an elegant and concise way in dependence and independence logic. The relationship between different properties and their simultaneous realisability can thus be formulated and proven on a purely logical level, as problems of entailment and satisfiability of logical formulae. Connections between probabilistic and relational entailment in dependence and independence logic allow us to simplify proofs. In many cases, we can establish results on both probabilistic and relational hidden-variable models by a single proof, because one case implies the other, depending on purely syntactic criteria. We also discuss the ‘no-go’ theorems by Bell and Kochen-Specker and provide a purely logical variant of the latter, introducing non-contextual choice as a team-semantical property.     

Kripke‐style Semantics of Orthomodular Logics

We present here a Kripke‐style semantics for propositional orthomodular logics that is based on the representation theorem for orthomodular lattices by D.J. Foulis ([2]), in which a sort of semigroups is employed. This semantics can characterize the logics above the orthomodular logic by some elementary conditions.     

Abstract Logics, Logic Maps, and Logic Homomorphisms

What is a logic? Which properties are preserved by maps between logics? What is the right notion for equivalence of logics? In order to give satisfactory answers we generalize and further develop the topological approach of [4] and present the foundations of a general theory of abstract logics which is based on the abstract concept of a theory. Each abstract logic determines a topology on the set of theories. We develop a theory of logic maps and show in what way they induce (continuous, open) functions on the corresponding topological spaces. We also establish connections to well-known notions such as translations of logics and the satisfaction axiom of institutions [5]. Logic homomorphisms are maps that behave in some sense like continuous functions and preserve more topological structure than logic maps in general. We introduce the notion of a logic isomorphism as a (not necessarily bijective) function on the sets of formulas that induces a homeomorphism between the respective topological spaces and gives rise to an equivalence relation on abstract logics. Therefore, we propose logic isomorphisms as an adequate and precise notion for equivalence of logics. Finally, we compare this concept with another recent proposal presented in [2]. This research was supported by the grant CNPq/FAPESB 350092/2006-0.     

Constructive modal logics I

We often have to draw conclusions about states of machines in computer science and about states of knowledge and belief in artificial intelligence (AI) based on partial information. Nerode (1990) suggested using constructive (equivalently, intuitionistic) logic as the language to express such deductions and also suggested designing appropriate intuitionistic Kripke frames to express the partial information. Following this program, Nerode and Wijesekera (1990) developed syntax, semantics and completeness for a system of intuitionistic dynamic logic for proving properties of concurrent programs. Like all dynamics logics, this was a logic of many modalities, each expressing a program, but in intuitionistic rather than in classical logic. In that logic, both box and diamond are needed, but these two are not intuitionistically interdefinable and, worse, diamond does not distribute over ‘or’, except for sequential programs. This also happens in other contemplated computer science and AI applications, and leads outside the class of constructive logics investigated in the literature. The present paper fills this gap. We provide intuitionistic logics with independent box and diamond without assuming distribution of diamond over ‘or’. The completeness theorem is based on intuitionistic Kripke frames (partially ordered sets of increasing worlds), but equipped with an additional, quite separate accessibility relation between worlds. In the interpretation of Nerode and Wijesekera (1990), worlds under the partial order represent states of partial knowledge, the accessibility represents change in state of partial knowledge resulting from executing a specific program. But there are many other computer science interpretations. This formalism covers all computer science applications of which we are aware. We also give a cut elimination theorem and algebraic and topological formulations, since these present some new difficulties. Finally, these results were obtained prior to those in Nerode and Wijesekera (1990).     

Incompleteness Results in Kripke Bundle Semantics

Kripke bundle and C-set semantics are known as semantics which generalize standard Kripke semantics. In [4] and in [1, 2] it is shown that Kripke bundle and C-set semantics are stronger than standard Kripke semantics. Also it is true that C-set semantics for superintuitionistic logics is stronger than Kripke bundle semantics ([6]). Modal predicate logic Q-S4.1 is not Kripke bundle complete ([3] - it is also yielded as a corollary to Theorem 6.1(a) of the present paper). This is shown by using difference of Kripke bundle semantics and C-set semantics. In this paper, by using the same idea we show that incompleteness results in Kripke bundle semantics which are extended versions of [2].