Logical operations and iterated infinitely deep languages

We discuss an abstract notion of a logical operation and corresponding logics. It is shown that if all the logical operations considered are implicitely definable in a logic ?*, then the same holds also for the logic obtained from these operations. As an application we show that certain iterated forms of infinitely deep languages are implicitely definable in game quantifier languages. We consider also relations between structures and show that Karttunen's characterization of elementary equivalence for the ordinary infinitely deep languages can be generalized to hold for the iterated infinitely deep languages. An early version of this work was presented in the Abstracts Section of ICM '78.     

Embedding Modal Nonmonotonic Logics into Default Logic

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

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.     

Expressivity of Imperfect Information Logics without Identity

In this article we investigate the family of independence-friendly (IF) logics in the equality-free setting, concentrating on questions related to expressive power. Various natural equality-free fragments of logics in this family translate into existential second-order logic with prenex quantification of function symbols only and with the first-order parts of formulae equality-free. We study this fragment of existential second-order logic. Our principal technical result is that over finite models with a vocabulary consisting of unary relation symbols only, this fragment of second-order logic is weaker in expressive power than first-order logic (with equality). Results about the fragment could turn out useful for example in the study of independence-friendly modal logics. In addition to proving results of a technical nature, we address issues related to a perspective from which IF logic is regarded as a specification framework for games, and also discuss the general significance of understanding fragments of second-order logic in investigations related to non-classical logics.     

A general tableau method for propositional interval temporal logics: Theory and implementation

In this paper, we focus our attention on tableau methods for propositional interval temporal logics. These logics provide a natural framework for representing and reasoning about temporal properties in several areas of computer science. However, while various tableau methods have been developed for linear and branching time point-based temporal logics, not much work has been done on tableau methods for interval-based ones. We develop a general tableau method for Venema's CDT logic interpreted over partial orders (BCDT⁺ for short). It combines features of the classical tableau method for first-order logic with those of explicit tableau methods for modal logics with constraint label management, and it can be easily tailored to most propositional interval temporal logics proposed in the literature. We prove its soundness and completeness, and we show how it has been implemented.     

Nelson's Negation on the Base of Weaker Versions of Intuitionistic Negation

Constructive logic with Nelson negation is an extension of the intuitionistic logic with a special type of negation expressing some features of constructive falsity and refutation by counterexample. In this paper we generalize this logic weakening maximally the underlying intuitionistic negation. The resulting system, called subminimal logic with Nelson negation, is studied by means of a kind of algebras called generalized N-lattices. We show that generalized N-lattices admit representation formalizing the intuitive idea of refutation by means of counterexamples giving in this way a counterexample semantics of the logic in question and some of its natural extensions. Among the extensions which are near to the intuitionistic logic are the minimal logic with Nelson negation which is an extension of the Johansson's minimal logic with Nelson negation and its in a sense dual version — the co-minimal logic with Nelson negation. Among the extensions near to the classical logic are the well known 3-valued logic of Lukasiewicz, two 12-valued logics and one 48-valued logic. Standard questions for all these logics — decidability, Kripke-style semantics, complete axiomatizability, conservativeness are studied. At the end of the paper extensions based on a new connective of self-dual conjunction and an analog of the Lukasiewicz middle value ½ have also been considered.     

Dialogue Games for Many-Valued Logics — an Overview

An overview of different versions and applications of Lorenzen’s dialogue game approach to the foundations of logic, here largely restricted to the realm of manyvalued logics, is presented. Among the reviewed concepts and results are Giles’s characterization of ?ukasiewicz logic and some of its generalizations to other fuzzy logics, including interval based logics, a parallel version of Lorenzen’s game for intuitionistic logic that is adequate for finite- and infinite-valued Gödel logics, and a truth comparison game for infinite-valued Gödel logic.     

Proof Systems for Reasoning about Computation Errors

In the paper we examine the use of non-classical truth values for dealing with computation errors in program specification and validation. In that context, 3-valued McCarthy logic is suitable for handling lazy sequential computation, while 3-valued Kleene logic can be used for reasoning about parallel computation. If we want to be able to deal with both strategies without distinguishing between them, we combine Kleene and McCarthy logics into a logic based on a non-deterministic, 3-valued matrix, incorporating both options as a non-deterministic choice. If the two strategies are to be distinguished, Kleene and McCarthy logics are combined into a logic based on a 4-valued deterministic matrix featuring two kinds of computation errors which correspond to the two computation strategies described above. For the resulting logics, we provide sound and complete calculi of ordinary, two-valued sequents. Presented by Yaroslav Shramko and Heinrich Wansing     

Modal Deduction in Second-Order Logic and Set Theory - II

In this paper, we generalize the set-theoretic translation method for poly-modal logic introduced in [11] to extended modal logics. Instead of devising an ad-hoc translation for each logic, we develop a general framework within which a number of extended modal logics can be dealt with. We first extend the basic set-theoretic translation method to weak monadic second-order logic through a suitable change in the underlying set theory that connects up in interesting ways with constructibility; then, we show how to tailor such a translation to work with specific cases of extended modal logics.     

从逻辑哲学看模糊逻辑的形式化

从逻辑哲学观点看,在“符号化、公理化的模糊逻辑”与非形式化的“人脑使用的模糊逻辑”（苗东升的说法）这两者之间,只是形式模型及其现实原型的关系,决不相互排斥。真正的问题不在于,在现实生活中人脑所使用的实际上行之有效的模糊推理,是否应该和可能符号化、公理化,而是在于如何恰当地进行形式化。笔者采用苏珊·哈克（Susan Haack）的逻辑哲学观点,认为非经典逻辑可划分为扩展逻辑和异常（deviation）逻辑,模糊逻辑归属于异常逻辑。本文以模糊逻辑系统FZ为例,具体分析了虽然经典逻辑中一些较强的公理和推理规则均不成立,但是与之对应的较弱的“合经典的”（well-behaved）公理和推理规则却仍然可以成立,由此导致一系列新奇性质。笔者采用了达·柯斯塔（da Costa）的形式化技巧,它是关于“在虚设不矛盾律成立的前提下”（相应公式可以称为“合经典的”）才能成立的逆否律。当我们撤除了“虚设不矛盾律为前提”的限定,它又重新回到了无条件成立的情况。笔者也推广了玻尔（N.Bohr）和冯·威扎克（von Weizsaecker）关于对应原理的思想,认为作为非经典逻辑的模糊逻辑与经典逻辑之间也应当遵守“对应原理”：经典逻辑是模糊逻辑的前身,模糊逻辑将构成更为普遍的逻辑形式,经典逻辑作为模糊逻辑的极限形式,在局部情况下还保持自身的意义。     

I. Psychologism,Functionalism, and the modal status of logical Laws

In a recent article (Inquiry, Vol. 19 [1976]), J. W. Meiland addresses the issue of psychologism in logic, which holds that logic is a branch of psychology and that logical laws (such as the Principle of Non‐Contradiction) are contingent upon the nature of the mind. Meiland examines Husserl's critique of psychologism, argues that Husserl is not convincing, and offers two new objections to the psychologistic thesis. In this paper I attempt to rebut those objections. In question are the acceptable criteria for determining the possibility or impossibility of systems of logic significantly different from our own. I argue that a criteriological application of our accepted laws of logic to this question commits a circular fallacy. I then argue that, even if we accept logical consistency as a criterion for possibility, a plausible argument for the possibility of valid alternative logics can be constructed by using the functionalist analogy between minds and automata. Finally, I attempt to rebut the claim that in logic the only changes possible are conceptual changes that would not permit a proposition to be both true and false.     

A Non-deterministic View on Non-classical Negations

We investigate two large families of logics, differing from each other by the treatment of negation. The logics in one of them are obtained from the positive fragment of classical logic (with or without a propositional constant ff for “the false”) by adding various standard Gentzen-type rules for negation. The logics in the other family are similarly obtained from LJ⁺, the positive fragment of intuitionistic logic (again, with or without ff). For all the systems, we provide simple semantics which is based on non-deterministic four-valued or three-valued structures, and prove soundness and completeness for all of them. We show that the role of each rule is to reduce the degree of non-determinism in the corresponding systems. We also show that all the systems considered are decidable, and our semantics can be used for the corresponding decision procedures. Most of the extensions of LJ⁺ (with or without ff) are shown to be conservative over the underlying logic, and it is determined which of them are not.     

Natural Deduction for Non-Classical Logics

We present a framework for machine implementation of families of non-classical logics with Kripke-style semantics. We decompose a logic into two interacting parts, each a natural deduction system: a base logic of labelled formulae, and a theory of labels characterizing the properties of the Kripke models. By appropriate combinations we capture both partial and complete fragments of large families of non-classical logics such as modal, relevance, and intuitionistic logics. Our approach is modular and supports uniform proofs of soundness, completeness and proof normalization. We have implemented our work in the Isabelle Logical Framework.     

Using Hybrid Logic for Coping with Functions in Subset Spaces

We extend Moss and Parikh’s modal logic for subset spaces by adding, among other things, state-valued and set-valued functions. This is done with the aid of some basic concepts from hybrid logic. We prove the soundness and completeness of the derived logics with regard to the class of all correspondingly enriched subset spaces, and show that these logics are decidable.     

Dual Equivalent Two-valued Under-determined and Over-determined Interpretations for Łukasiewicz’s 3-valued Logic Ł3

?ukasiewicz three-valued logic ?3 is often understood as the set of all 3-valued valid formulas according to ?ukasiewicz’s 3-valued matrices. Following Wojcicki, in addition, we shall consider two alternative interpretations of ?3: “well-determined” ?3a and “truth-preserving” ?3b defined by two different consequence relations on the 3-valued matrices. The aim of this paper is to provide (by using Dunn semantics) dual equivalent two-valued under-determined and over-determined interpretations for ?3, ?3a and ?3b. The logic ?3 is axiomatized as an extension of Routley and Meyer’s basic positive logic following Brady’s strategy for axiomatizing many-valued logics by employing two-valued under-determined or over-determined interpretations. Finally, it is proved that “well determined” ?ukasiewicz logics are paraconsistent.     

A logical formalization of the OCC theory of emotions

In this paper, we provide a logical formalization of the emotion triggering process and of its relationship with mental attitudes, as described in Ortony, Clore, and Collins’s theory. We argue that modal logics are particularly adapted to represent agents’ mental attitudes and to reason about them, and use a specific modal logic that we call Logic of Emotions in order to provide logical definitions of all but two of their 22 emotions. While these definitions may be subject to debate, we show that they allow to reason about emotions and to draw interesting conclusions from the theory.     

Action negation and alternative reductions for dynamic deontic logics

Dynamic deontic logics reduce normative assertions about explicit complex actions to standard dynamic logic assertions about the relation between complex actions and violation conditions. We address two general, but related problems in this field. The first is to find a formalization of the notion of ‘action negation’ that (1) has an intuitive interpretation as an action forming combinator and (2) does not impose restrictions on the use of other relevant action combinators such as sequence and iteration, and (3) has a meaningful interpretation in the normative context. The second problem we address concerns the reduction from deontic assertions to dynamic logic assertions. Our first point is that we want this reduction to obey the free-choice semantics for norms. For ought-to-be deontic logics it is generally accepted that the free-choice semantics is counter-intuitive. But for dynamic deontic logics we actually consider it a viable, if not, the better alternative. Our second concern with the reduction is that we want it to be more liberal than the ones that were proposed before in the literature. For instance, Meyer's reduction does not leave room for action whose normative status is neither permitted nor forbidden. We test the logics we define in this paper against a set of minimal logic requirements.     

Inquisitive Heyting Algebras

In this paper we introduce a class of inquisitive Heyting algebras as algebraic structures that are isomorphic to algebras of finite antichains of bounded implicative meet semilattices. It is argued that these structures are suitable for algebraic semantics of inquisitive superintuitionistic logics, i.e. logics of questions based on intuitionistic logic and its extensions. We explain how questions are represented in these structures (prime elements represent declarative propositions, non-prime elements represent questions, join is a question-forming operation) and provide several alternative characterizations of these algebras. For instance, it is shown that a Heyting algebra is inquisitive if and only if its prime filters and filters generated by sets of prime elements coincide and prime elements are closed under relative pseudocomplement. We prove that the weakest inquisitive superintuitionistic logic is sound with respect to a Heyting algebra iff the algebra is what we call a homomorphic p-image of some inquisitive Heyting algebra. It is also shown that a logic is inquisitive iff its Lindenbaum–Tarski algebra is an inquisitive Heyting algebra.