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.     

Uniform interpolation and the existence of sequent calculi

This paper presents a uniform and modular method to prove uniform interpolation for several intermediate and intuitionistic modal logics. The proof-theoretic method uses sequent calculi that are extensions of the terminating sequent calculus $\mathsf{G4ip}$ for intuitionistic propositional logic. It is shown that whenever the rules in a calculus satisfy certain structural properties, the corresponding logic has uniform interpolation. It follows that the intuitionistic versions of $\mathsf{K}$ and $\mathsf{KD}$ (without the diamond operator) have uniform interpolation. It also follows that no intermediate or intuitionistic modal logic without uniform interpolation has a sequent calculus satisfying those structural properties, thereby establishing that except for the seven intermediate logics that have uniform interpolation, no intermediate logic has such a sequent calculus.     

Modularity results for interpolation,amalgamation and superamalgamation

Wolter in [38] proved that the Craig interpolation property transfers to fusion of normal modal logics. It is well-known [21] that for such logics Craig interpolation corresponds to an algebraic property called superamalgamability. In this paper, we develop model-theoretic techniques at the level of first-order theories in order to obtain general combination results transferring quantifier-free interpolation to unions of theories over non-disjoint signatures. Such results, once applied to equational theories sharing a common Boolean reduct, can be used to prove that superamalgamability is modular also in the non-normal case. We also state that, in this non-normal context, superamalgamability corresponds to a strong form of interpolation that we call “comprehensive interpolation property” (which consequently transfers to fusions).     

Evidence and plausibility in neighborhood structures

The intuitive notion of evidence has both semantic and syntactic features. In this paper, we develop an evidence logic for epistemic agents faced with possibly contradictory evidence from different sources. The logic is based on a neighborhood semantics, where a neighborhood N indicates that the agent has reason to believe that the true state of the world lies in N. Further notions of relative plausibility between worlds and beliefs based on the latter ordering are then defined in terms of this evidence structure, yielding our intended models for evidence-based beliefs. In addition, we also consider a second more general flavor, where belief and plausibility are modeled using additional primitive relations, and we prove a representation theorem showing that each such general model is a p-morphic image of an intended one. This semantics invites a number of natural special cases, depending on how uniform we make the evidence sets, and how coherent their total structure. We give a structural study of the resulting ‘uniform’ and ‘flat’ models. Our main result are sound and complete axiomatizations for the logics of all four major model classes with respect to the modal language of evidence, belief and safe belief. We conclude with an outlook toward logics for the dynamics of changing evidence, and the resulting language extensions and connections with logics of plausibility change.     

On the interpolation property of some intuitionistic modal logics

LetL be one of the intuitionistic modal logics considered in [7] (or one of its extensions) and letM _L be the algebraic semantics ofL. In this paper we will extend toL the equivalence, proved in the classical case (see [6]), among he weak Craig interpolation theorem, the Robinson theorem and the amalgamation property of varietyM _L. We will also prove the equivalence between the Craig interpolation theorem and the super-amalgamation property of varietyM _L. Then we obtain the Craig interpolation theorem and Robinson theorem for two intuitionistic modal logics, one ofS ₄-type and the other one ofS ₅-type, showing the super-amalgamation property of the corresponding algebraic semantics.     

Glivenko theorems revisited

Glivenko-type theorems for substructural logics (over FL) are comprehensively studied in the paper [N. Galatos, H. Ono, Glivenko theorems for substructural logics over FL, Journal of Symbolic Logic 71 (2006) 1353-1384]. Arguments used there are fully algebraic, and based on the fact that all substructural logics are algebraizable (see [N. Galatos, H. Ono, Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL, Studia Logica 83 (2006) 279-308] and also [N. Galatos, P. Jipsen, T. Kowalski, H. Ono, Residuated Lattices: An Algebraic Glimpse at Substructural Logics, in: Studies in Logic and the Foundations of Mathematics, vol. 151, Elsevier, 2007] for the details).As a complementary work to the algebraic approach developed in [N. Galatos, H. Ono, Glivenko theorems for substructural logics over FL, Journal of Symbolic Logic 71 (2006) 1353-1384], we present here a concise, proof-theoretic approach to Glivenko theorems for substructural logics. This will show different features of these two approaches.     

Modules over quantaloids: Applications to the isomorphism problem in algebraic logic and π-institutions

We solve the isomorphism problem in the context of abstract algebraic logic and of π-institutions, namely the problem of when the notions of syntactic and semantic equivalence among logics coincide. The problem is solved in the general setting of categories of modules over quantaloids. We introduce closure operators on modules over quantaloids and their associated morphisms. We show that, up to isomorphism, epis are morphisms associated with closure operators. The notions of (semi-)interpretability and (semi-)representability are introduced and studied. We introduce cyclic modules, and provide a characterization for cyclic projective modules as those having a g-variable. Finally, we explain how every π-institution induces a module over a quantaloid, and thus the theory of modules over quantaloids can be considered as an abstraction of the theory of π-institutions.     

On the rules of intermediate logics

If the Visser rules are admissible for an intermediate logic, they form a basis for the admissible rules of the logic. How to characterize the admissible rules of intermediate logics for which not all of the Visser rules are admissible is not known. In this paper we give a brief overview of results on admissible rules in the context of intermediate logics. We apply these results to some well-known intermediate logics. We provide natural examples of logics for which the Visser rule are derivable, admissible but nonderivable, or not admissible. Supported by the Austrian Science Fund FWF under projects P16264 and P16539.     

Craig interpolation for semilinear substructural logics

The Craig interpolation property is investigated for substructural logics whose algebraic semantics are varieties of semilinear (subdirect products of linearly ordered) pointed commutative residuated lattices. It is shown that Craig interpolation fails for certain classes of these logics with weakening if the corresponding algebras are not idempotent. A complete characterization is then given of axiomatic extensions of the “R‐mingle with unit” logic (corresponding to varieties of Sugihara monoids) that have the Craig interpolation property. This latter characterization is obtained using a model‐theoretic quantifier elimination strategy to determine the varieties of Sugihara monoids admitting the amalgamation property.     

Effectiveness in RPL, with applications to continuous logic

In this paper, we introduce a foundation for computable model theory of rational Pavelka logic (an extension of ?ukasiewicz logic) and continuous logic, and prove effective versions of some related theorems in model theory. We show how to reduce continuous logic to rational Pavelka logic. We also define notions of computability and decidability of a model for logics with computable, but uncountable, set of truth values; we show that provability degree of a formula with respect to a linear theory is computable, and use this to carry out an effective Henkin construction. Therefore, for any effectively given consistent linear theory in continuous logic, we effectively produce its decidable model. This is the best possible, since we show that the computable model theory of continuous logic is an extension of computable model theory of classical logic. We conclude with noting that the unique separable model of a separably categorical and computably axiomatizable theory (such as that of a probability space or an L^p Banach lattice) is decidable.     

The logic of justified belief,explicit knowledge,and conclusive evidence

We present a complete, decidable logic for reasoning about a notion of completely trustworthy (“conclusive”) evidence and its relations to justifiable (implicit) belief and knowledge, as well as to their explicit justifications. This logic makes use of a number of evidence-related notions such as availability, admissibility, and “goodness” of a piece of evidence, and is based on an innovative modification of the Fitting semantics for Artemov?s Justification Logic designed to preempt Gettier-type counterexamples. We combine this with ideas from belief revision and awareness logics to provide an account for explicitly justified (defeasible) knowledge based on conclusive evidence that addresses the problem of (logical) omniscience.     

Prefixed tableaus and nested sequents

Nested sequent systems for modal logics are a relatively recent development, within the general area known as deep reasoning. The idea of deep reasoning is to create systems within which one operates at lower levels in formulas than just those involving the main connective or operator. Prefixed tableaus go back to 1972, and are modal tableau systems with extra machinery to represent accessibility in a purely syntactic way. We show that modal nested sequents and prefixed modal tableaus are notational variants of each other, roughly in the same way that Gentzen sequent calculi and tableaus are notational variants. This immediately gives rise to new modal nested sequent systems which may be of independent interest. We discuss some of these, including those for some justification logics that include standard modal operators.     

A focused approach to combining logics

We present a compact sequent calculus LKU for classical logic organized around the concept of polarization. Focused sequent calculi for classical, intuitionistic, and multiplicative-additive linear logics are derived as fragments of the host system by varying the sensitivity of specialized structural rules to polarity information. We identify a general set of criteria under which cut-elimination holds in such fragments. From cut-elimination we derive a unified proof of the completeness of focusing. Furthermore, each sublogic can interact with other fragments through cut. We examine certain circumstances, for example, in which a classical lemma can be used in an intuitionistic proof while preserving intuitionistic provability. We also examine the possibility of defining classical-linear hybrid logics.     

Inclusion and exclusion dependencies in team semantics — On some logics of imperfect information

We introduce some new logics of imperfect information by adding atomic formulas corresponding to inclusion and exclusion dependencies to the language of first order logic. The properties of these logics and their relationships with other logics of imperfect information are then studied. As a corollary of these results, we characterize the expressive power of independence logic, thus answering an open problem posed in Grädel and Väänänen, 2010 [9].     

Labeled sequent calculus for justification logics

Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for combined modal-justification logics. Using a method due to Sara Negri, we internalize the Kripke-style semantics of justification and modal-justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculi. We show that all rules of these systems are invertible and the structural rules (weakening and contraction) and the cut rule are admissible. Soundness and completeness are established as well. The analyticity for some of our labeled sequent calculi are shown by proving that they enjoy the subformula, sublabel and subterm properties. We also present an analytic labeled sequent calculus for $\mathsf{S4LPN}$ based on Artemov–Fitting models.     

The Lyndon property and uniform interpolation over the Grzegorczyk logic

We consider versions of the interpolation property stronger than the Craig interpolation property and prove the Lyndon interpolation property for the Grzegorczyk logic and some of its extensions. We also establish the Lyndon interpolation property for most extensions of the intuitionistic logic with Craig interpolation property. For all modal logics over the Grzegorczyk logic as well as for all superintuitionistic logics, the uniform interpolation property is equivalent to Craig’s property.     

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.     

On the classification of first order Gödel logics

We characterize the recursively enumerable first order Gödel logics with △ with respect to validity and non-satisfiability. The finitely valued and four infinitely valued Gödel logics with △ are recursively enumerable, not-satisfiability is recursively enumerable if validity is recursively enumerable. This is in contrast to first order Gödel logics without △, where validity is recursively enumerable for finitely valued and two infinitely valued Gödel logics, not-satisfiability is recursively enumerable if validity is recursively enumerable or 0 isolated in the truth value set.     

Note on witnessed Gödel logics with Delta

Witnessed Gödel logics are based on the interpretation of ∀ (∃) by minimum (maximum) instead of supremum (infimum). Witnessed Gödel logics appear for many practical purposes more suited than usual Gödel logics as the occurrence of proper infima/suprema is practically irrelevant. In this note we characterize witnessed Gödel logics with absoluteness operator △ w.r.t. witnessed Gödel logics using a uniform translation.     

Paley Type Inequalities for Orthogonal Series with Vector-Valued Coefficients

We investigate the extension to Banach-space-valued functions of the classical inequalities due to Paley for the Fourier coefficients with respect to a general orthonormal system Φ. This leads us to introduce the notions of Paley Φ-type and Φ-cotype for a Banach space and some related concepts. We study the relations between these notions of type and cotype and those previously defined. We also analyze how the interpolation spaces inherit these characteristics from the original spaces, and use them to obtain sharp coefficient estimates for functions taking values in Lorentz spaces.