Algebraic semantics and model completeness for Intuitionistic Public Announcement Logic

In the present paper, we start studying epistemic updates using the standard toolkit of duality theory. We focus on public announcements, which are the simplest epistemic actions, and hence on Public Announcement Logic (PAL) without the common knowledge operator. As is well known, the epistemic action of publicly announcing a given proposition is semantically represented as a transformation of the model encoding the current epistemic setup of the given agents; the given current model being replaced with its submodel relativized to the announced proposition. We dually characterize the associated submodel-injection map as a certain pseudo-quotient map between the complex algebras respectively associated with the given model and with its relativized submodel. As is well known, these complex algebras are complete atomic BAOs (Boolean algebras with operators). The dual characterization we provide naturally generalizes to much wider classes of algebras, which include, but are not limited to, arbitrary BAOs and arbitrary modal expansions of Heyting algebras (HAOs). Thanks to this construction, the benefits and the wider scope of applications given by a point-free, intuitionistic theory of epistemic updates are made available. As an application of this dual characterization, we axiomatize the intuitionistic analogue of PAL, which we refer to as IPAL, prove soundness and completeness of IPAL w.r.t. both algebraic and relational models, and show that the well known Muddy Children Puzzle can be formalized in IPAL.     

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.     

Arithmetical complexity of fuzzy predicate logics — A survey II

Results on arithmetical complexity of important sets of formulas of several fuzzy predicate logics (tautologies, satisfiable formulas, …) are surveyed and some new results are proven.     

Projective limits of MV-spaces

An MV-space is a topological space X such that there exists an MV-algebra A whose prime spectrum Spec A is homeomorphic to X. The characterization of the MV-spaces is an important open problem.We shall prove that any projective limit of MV-spaces in the category of spectral spaces is an MV-space. In this way, we obtain new classes of MV-spaces related to some preservation properties of the Belluce functor.     

A complete many-valued logic with product-conjunction

A simple complete axiomatic system is presented for the many-valued propositional logic based on the conjunction interpreted as product, the coresponding implication (Goguen's implication) and the corresponding negation (Gödel's negation). Algebraic proof methods are used. The meaning for fuzzy logic (in the narrow sense) is shortly discussed.This article was processed by the author using the LATEX style filepljorlm from Springer-Verlag.     

MV-algebras: a variety for magnitudes with archimedean units

Chang’s MV-algebras, on the one hand, are the algebras of the infinite-valued Łukasiewicz calculus and, on the other hand, are categorically equivalent to abelian lattice-ordered groups with a distinguished strong unit, for short, unital ℓ-groups. The latter are a modern mathematization of the time-honored euclidean magnitudes with an archimedean unit. While for magnitudes the unit is no less important than the zero element, its archimedean property is not even definable in first-order logic. This gives added interest to the equivalent representation of unital ℓ-groups via the equational class of MV-algebras. In this paper we survey several applications of this equivalence, and various properties of the variety of MV-algebras.Dedicated to the Memory of Wim BlokReceived August 26, 2003; accepted in final form October 3, 2004.This revised version was published online in August 2005 with a corrected cover date.     

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.     

Sufficient triangular norms in many-valued logics with standard negation

In many-valued logics with the unit interval as the set of truth values, from the standard negation and the product (or, more generally, from any strict Frank t-norm) all measurable logical functions can be derived, provided that also operations with countable arity are allowed. The question remained open whether there are other t-norms with this property or whether all strict t-norms possess this property. We give a full solution to this problem (in the case of strict t-norms), together with convenient sufficient conditions. We list several families of strict t-norms having this property and provide also counterexamples (the Hamacher product is one of them). Finally, we discuss the consequences of these results for the characterization of tribes based on strict t-norms.     

Imperative programs as proofs via game semantics

Game semantics extends the Curry–Howard isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this paper we describe a logical counterpart to this extension, in which proofs denote such strategies. The system is expressive: it contains all of the connectives of Intuitionistic Linear Logic, and first-order quantification. Use of Laird?s sequoid operator allows proofs with imperative behaviour to be expressed. Thus, we can embed first-order Intuitionistic Linear Logic into this system, Polarized Linear Logic, and an imperative total programming language.     

Canonical extensions for congruential logics with the deduction theorem

We introduce a new and general notion of canonical extension for algebras in the algebraic counterpart of any finitary and congruential logic S. This definition is logic-based rather than purely order-theoretic and is in general different from the definition of canonical extensions for monotone poset expansions, but the two definitions agree whenever the algebras in are based on lattices. As a case study on logics purely based on implication, we prove that the varieties of Hilbert and Tarski algebras are canonical in this new sense.     

Completeness for flat modal fixpoint logics

This paper exhibits a general and uniform method to prove axiomatic completeness for certain modal fixpoint logics. Given a set Γ of modal formulas of the form γ(x,p₁,…,p_n), where x occurs only positively in γ, we obtain the flat modal fixpoint language L_?(Γ) by adding to the language of polymodal logic a connective ?_γ for each γ∈Γ. The term ?_γ(φ₁,…,φ_n) is meant to be interpreted as the least fixed point of the functional interpretation of the term γ(x,φ₁,…,φ_n). We consider the following problem: given Γ, construct an axiom system which is sound and complete with respect to the concrete interpretation of the language L_?(Γ) on Kripke structures. We prove two results that solve this problem.First, let be the logic obtained from the basic polymodal by adding a Kozen-Park style fixpoint axiom and a least fixpoint rule, for each fixpoint connective ?_γ. Provided that each indexing formula γ satisfies a certain syntactic criterion, we prove this axiom system to be complete.Second, addressing the general case, we prove the soundness and completeness of an extension of . This extension is obtained via an effective procedure that, given an indexing formula γ as input, returns a finite set of axioms and derivation rules for ?_γ, of size bounded by the length of γ. Thus the axiom system is finite whenever Γ is finite.     

Algebraic proof theory for substructural logics: Cut-elimination and completions

We carry out a unified investigation of two prominent topics in proof theory and order algebra: cut-elimination and completion, in the setting of substructural logics and residuated lattices.We introduce the substructural hierarchy — a new classification of logical axioms (algebraic equations) over full Lambek calculus FL, and show that a stronger form of cut-elimination for extensions of FL and the MacNeille completion for subvarieties of pointed residuated lattices coincide up to the level N₂ in the hierarchy. Negative results, which indicate limitations of cut-elimination and the MacNeille completion, as well as of the expressive power of structural sequent calculus rules, are also provided.Our arguments interweave proof theory and algebra, leading to an integrated discipline which we call algebraic proof theory.     

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.     

Subreducts of MV-algebras with product and product residuation

Recently, MV-algebras with product have been investigated from different points of view. In particular, in [EGM01], a variety resulting from the combination of MV-algebras and product algebras (see [H98]) has been introduced. The elements of this variety are called ŁΠ-algebras. In this paper we treat subreducts of ŁΠ-algebras, with emphasis on quasivarieties of subreducts whose basic operations are continuous in the order topology. We give axiomatizations of the most interesting classes of subreducts, and we connect them with other algebraic classes of algebras, like f-rings and Wajsberg hoops, as well as to structures of co-infinitesimals of ŁΠ-algebras. In some cases, connections are given by means of equivalences of categories.Dedicated to the Memory of Wim BlokReceived June 19, 2002; accepted in final form November 29, 2004.This revised version was published online in August 2005 with a corrected cover date.     

Cut elimination and strong separation for substructural logics: An algebraic approach

We develop a general algebraic and proof-theoretic study of substructural logics that may lack associativity, along with other structural rules. Our study extends existing work on (associative) substructural logics over the full Lambek Calculus (see, for example, Ono (2003) [34], Galatos and Ono (2006) [18], Galatos et al. (2007) [17]). We present a Gentzen-style sequent system that lacks the structural rules of contraction, weakening, exchange and associativity, and can be considered a non-associative formulation of . Moreover, we introduce an equivalent Hilbert-style system and show that the logic associated with and is algebraizable, with the variety of residuated lattice-ordered groupoids with unit serving as its equivalent algebraic semantics.Overcoming technical complications arising from the lack of associativity, we introduce a generalized version of a logical matrix and apply the method of quasicompletions to obtain an algebra and a quasiembedding from the matrix to the algebra. By applying the general result to specific cases, we obtain important logical and algebraic properties, including the cut elimination of and various extensions, the strong separation of , and the finite generation of the variety of residuated lattice-ordered groupoids with unit.     

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].     

Generalized ordinal sums and the decidability of BL-chains

We present a general construction of a family of ordinal sums of a sequence of structures and prove an elimination theorem for the class of ordinal sums in an expanded language. From this we deduce the decidability of the class of -ordinal sums of models of a decidable theory T. As an application of this result we prove that the theory of BL-chains is decidable.In Celebration of the Sixtieth Birthday of Ralph N. McKenzieReceived June 9, 2002; accepted in final form June 19, 2003.     

Decomposition of BL-chains

A simple and self contained proof of decomposition of BL-chains into ordinal sums of Wajsberg hoops is given.Received October 23, 2003; accepted in final form September 11, 2004.