Term-Modal Logics

Many powerful logics exist today for reasoning about multi-agent systems, but in most of these it is hard to reason about an infinite or indeterminate number of agents. Also the naming schemes used in the logics often lack expressiveness to name agents in an intuitive way.To obtain a more expressive language for multi-agent reasoning and a better naming scheme for agents, we introduce a family of logics called term-modal logics. A main feature of our logics is the use of modal operators indexed by the terms of the logics. Thus, one can quantify over variables occurring in modal operators. In term-modal logics agents can be represented by terms, and knowledge of agents is expressed with formulas within the scope of modal operators.This gives us a flexible and uniform language for reasoning about the agents themselves and their knowledge. This article gives examples of the expressiveness of the languages and provides sequent-style and tableau-based proof systems for the logics. Furthermore we give proofs of soundness and completeness with respect to the possible world semantics.     

On the Algebraizability of Annotated Logics

Annotated logics were introduced by V.S. Subrahmanian as logical foundations for computer programming. One of the difficulties of these systems from the logical point of view is that they are not structural, i.e., their consequence relations are not closed under substitutions. In this paper we give systems of annotated logics that are equivalent to those of Subrahmanian in the sense that everything provable in one type of system has a translation that is provable in the other. Moreover these new systems are structural. We prove that these systems are weakly congruential, namely, they have an infinite system of congruence 1-formulas. Moreover, we prove that an annotated logic is algebraizable (i.e., it has a finite system of congruence formulas,) if and only if the lattice of annotation constants is finite.     

Definability and Interpolation in Non-Classical Logics

Algebraic approach to study of classical and non-classical logical calculi was developed and systematically presented by Helena Rasiowa in [48], [47]. It is very fruitful in investigation of non-classical logics because it makes possible to study large families of logics in an uniform way. In such research one can replace logics with suitable classes of algebras and apply powerful machinery of universal algebra. In this paper we present an overview of results on interpolation and definability in modal and positive logics,and also in extensions of Johansson's minimal logic. All these logics are strongly complete under algebraic semantics. It allows to combine syntactic methods with studying varieties of algebras and to flnd algebraic equivalents for interpolation and related properties. Moreover, we give exhaustive solution to interpolation and some related problems for many families of propositional logics and calculi. This paper is a version of the invited talk given by the author at the conference Trends in Logic III, dedicated to the memory of A. MOSTOWSKI, H. RASIOWA and C. RAUSZER, and held in Warsaw and Ruciane-Nida from 23rd to 25th September 2005. Presented by Jacek Malinowski     

Selfextensional Logics with a Conjunction

A logic is selfextensional if its interderivability (or mutual consequence) relation is a congruence relation on the algebra of formulas. In the paper we characterize the selfextensional logics with a conjunction as the logics that can be defined using the semilattice order induced by the interpretation of the conjunction in the algebras of their algebraic counterpart. Using the charactrization we provide simpler proofs of several results on selfextensional logics with a conjunction obtained in [13] using Gentzen systems. We also obtain some results on Fregean logics with conjunction.This paper is a version of the invited talk at the conference Trends in Logic III, dedicated to the memory of A. MOSTOWSKI, H. RASIOWA and C. RRAUSZER, and held in Warsaw and Ruciane-Nida from 23rd to 25th September 2005.     

Behavioral Algebraization of Logics

We introduce and study a new approach to the theory of abstract algebraic logic (AAL) that explores the use of many-sorted behavioral logic in the role traditionally played by unsorted equational logic. Our aim is to extend the range of applicability of AAL toward providing a meaningful algebraic counterpart also to logics with a many-sorted language, and possibly including non-truth-functional connectives. The proposed behavioral approach covers logics which are not algebraizable according to the standard approach, while also bringing a new algebraic perspective to logics which are algebraizable using the standard tools of AAL. Furthermore, we pave the way toward a robust behavioral theory of AAL, namely by providing a behavioral version of the Leibniz operator which allows us to generalize the traditional Leibniz hierarchy, as well as several well-known characterization results. A number of meaningful examples will be used to illustrate the novelties and advantages of the approach. Presented by Daniele Mundici     

On Modal Logics of Partial Recursive Functions

The classical propositional logic is known to be sound and complete with respect to the set semantics that interprets connectives as set operations. The paper extends propositional language by a new binary modality that corresponds to partial recursive function type constructor under the above interpretation. The cases of deterministic and non-deterministic functions are considered and for both of them semantically complete modal logics are described and decidability of these logics is established. Presented by Melvin Fitting     

A Generic Framework for Adaptive Vague Logics

In this paper, we present a generic format for adaptive vague logics. Logics based on this format are able to (1) identify sentences as vague or non-vague in light of a given set of premises, and to (2) dynamically adjust the possible set of inferences in accordance with these identifications, i.e. sentences that are identified as vague allow only for the application of vague inference rules and sentences that are identified as non-vague also allow for the application of some extra set of classical logic rules. The generic format consists of a set of minimal criteria that must be satisfied by the vague logic in casu in order to be usable as a basis for an adaptive vague logic. The criteria focus on the way in which the logic deals with a special ⊡-operator. Depending on the kind of logic for vagueness that is used as a basis for the adaptive vague logic, this operator can be interpreted as completely true, definitely true, clearly true, etc. It is proven that a wide range of famous logics for vagueness satisfies these criteria when extended with a specific ⊡-operator, e.g. fuzzy basic logic and its well known extensions, cf. [7], super- and subvaluationist logics, cf. [6], [9], and clarity logic, cf. [13]. Also a fuzzy logic is presented that can be used for an adaptive vague logic that can deal with higher-order vagueness. To illustrate the theory, some toy-examples of adaptive vague proofs are provided.     

Combinator Logics

Combinator logics are a broad family of substructual logics that are formed by extending the basic relevant logic B with axioms that correspond closely to the reduction rules of proper combinators in combinatory logic. In the Routley-Meyer relational semantics for relevant logic each such combinator logic is characterized by the class of frames that meet a first-order condition that also directly corresponds to the same combinator's reduction rule. A second family of logics is also introduced that extends B with the addition of propositional constants that correspond to combinators. These are characterized by relational frames that meet first-order conditions that reflect the structures of the combinators themselves.     

Predicate Logics on Display

The paper provides a uniform Gentzen-style proof-theoretic framework for various subsystems of classical predicate logic. In particular, predicate logics obtained by adopting van Behthem's modal perspective on first-order logic are considered. The Gentzen systems for these logics augment Belnap's display logic by introduction rules for the existential and the universal quantifier. These rules for x and x are analogous to the display introduction rules for the modal operators and and do not themselves allow the Barcan formula or its converse to be derived. En route from the minimal modal predicate logic to full first-order logic, axiomatic extensions are captured by purely structural sequent rules.     

On Dynamic Topological and Metric Logics

We investigate computational properties of propositional logics for dynamical systems. First, we consider logics for dynamic topological systems (W.f), fi, where W is a topological space and f a homeomorphism on W. The logics come with ‘modal’ operators interpreted by the topological closure and interior, and temporal operators interpreted along the orbits {w, f(w), f² (w), ˙˙˙} of points w ε W. We show that for various classes of topological spaces the resulting logics are not recursively enumerable (and so not recursively axiomatisable). This gives a ‘negative’ solution to a conjecture of Kremer and Mints. Second, we consider logics for dynamical systems (W, f), where W is a metric space and f and isometric function. The operators for topological interior/closure are replaced by distance operators of the form ‘everywhere/somewhere in the ball of radius a, ‘for a ε Q ⁺. In contrast to the topological case, the resulting logic turns out to be decidable, but not in time bounded by any elementary function.     

Predicate Logical Extensions of some Subintuitionistic Logics

The paper presents predicate logical extensions of some subintuitionistic logics. Subintuitionistic logics result if conditions of the accessibility relation in Kripke models for intuitionistic logic are dropped. The accessibility relation which interprets implication in models for the propositional base subintuitionistic logic considered here is neither persistent on atoms, nor reflexive, nor transitive. Strongly complete predicate logical extensions are modeled with a second accessibility relation, which is a partial order, for the interpretation of the universal quantifier. Presented by Melvin Fitting     

Normal Modal Substructural Logics with Strong Negation

We introduce modal propositional substructural logics with strong negation, and prove the completeness theorems (with respect to Kripke models) for these logics.     

All Finitely Axiomatizable Tense Logics of Linear Time Flows Are CoNP-complete

We prove that all finitely axiomatizable tense logics with temporal operators for ‘always in the future’ and ‘always in the past’ and determined by linear fows time are coNP-complete. It follows, for example, that all tense logics containing a density axiom of the form ■ⁿ⁺¹_F p → ⁿ_F p, for some n ≥ 0, are coNP-complete. Additionally, we prove coNP-completeness of all ∩-irreducible tense logics. As these classes of tense logics contain many Kripke incomplete bimodal logics, we obtain many natural examples of Kripke incomplete normal bimodal logics which are nevertheless coNP-complete.     

Embedding Modal Nonmonotonic Logics into Default Logic

We present a straightforward embedding of modal nonmonotonic logics into default logic.     

Synonymous Logics

This paper discusses the general problem of translation functions between logics, given in axiomatic form, and in particular, the problem of determining when two such logics are synonymous or translationally equivalent. We discuss a proposed formal definition of translational equivalence, show why it is reasonable, and also discuss its relation to earlier definitions in the literature. We also give a simple criterion for showing that two modal logics are not translationally equivalent, and apply this to well-known examples. Some philosophical morals are drawn concerning the possibility of having two logical systems that are empirically distinct but are both translationally equivalent to a common logic.     

A Theory of Hypermodal Logics: Mode Shifting in Modal Logic

A hypermodality is a connective whose meaning depends on where in the formula it occurs. The paper motivates the notion and shows that hypermodal logics are much more expressive than traditional modal logics. In fact we show that logics with very simple K hypermodalities are not complete for any neighbourhood frames.     

Many-Valued Logics and Suszko's Thesis Revisited

Suszko's Thesis maintains that many-valued logics do not exist at all. In order to support it, R. Suszko offered a method for providing any structural abstract logic with a complete set of bivaluations. G. Malinowski challenged Suszko's Thesis by constructing a new class of logics (called q-logics by him) for which Suszko's method fails. He argued that the key for logical two-valuedness was the "bivalent" partition of the Lindenbaum bundle associated with all structural abstract logics, while his q-logics were generated by "trivalent" matrices. This paper will show that contrary to these intuitions, logical two-valuedness has more to do with the geometrical properties of the deduction relation of a logical structure than with the algebraic properties embedded on it.     

Synchronization of Logics

Motivated by applications in software engineering, we propose two forms of combination of logics: synchronization on formulae and synchronization on models. We start by reviewing satisfaction systems, consequence systems, one-step derivation systems and theory spaces, as well as their functorial relationships. We define the synchronization on formulae of two consequence systems and provide a categorial characterization of the construction. For illustration we consider the synchronization of linear temporal logic and equational logic. We define the synchronization on models of two satisfaction systems and provide a categorial characterization of the construction. We illustrate the technique in two cases: linear temporal logic versus equational logic; and linear temporal logic versus branching temporal logic. Finally, we lift the synchronization on formulae to the category of logics over consequences systems.     

On Retaining Classical Truths and Classical Deducibility in Many-Valued and Fuzzy Logics

In this paper, I identify the source of the differences between classical logic and many-valued logics (including fuzzy logics) with respect to the set of valid formulas and the set of inferences sanctioned. In the course of doing so, we find the conditions that are individually necessary and jointly sufficient for any many-valued semantics (again including fuzzy logics) to validate exactly the classically valid formulas, while sanctioning exactly the same set of inferences as classical logic. This in turn shows, contrary to what has sometimes been claimed, that at least one class of infinite-valued semantics is axiomatizable.     

Notes on Logics of Metric Spaces

In [14], we studied the computational behaviour of various first-order and modal languages interpreted in metric or weaker distance spaces. [13] gave an axiomatisation of an expressive and decidable metric logic. The main result of this paper is in showing that the technique of representing metric spaces by means of Kripke frames can be extended to cover the modal (hybrid) language that is expressively complete over metric spaces for the (undecidable) two-variable fragment of first-order logic with binary pred-icates interpreting the metric. The frame conditions needed correspond rather directly with a Boolean modal logic that is, again, of the same expressivity as the two-variable fragment. We use this representation to derive an axiomatisation of the modal hybrid variant of the two-variable fragment, discuss the compactness property in distance logics, and derive some results on (the failure of) interpolation in distance logics of various expressive power. Presented by Melvin Fitting