A Kripke Semantics for the Logic of Gelfand Quantales

Gelfand quantales are complete unital quantales with an involution, *, satisfying the property that for any element a, if a b a for all b, then a a* a = a. A Hilbert-style axiom system is given for a propositional logic, called Gelfand Logic, which is sound and complete with respect to Gelfand quantales. A Kripke semantics is presented for which the soundness and completeness of Gelfand logic is shown. The completeness theorem relies on a Stone style representation theorem for complete lattices. A Rasiowa/Sikorski style semantic tableau system is also presented with the property that if all branches of a tableau are closed, then the formula in question is a theorem of Gelfand Logic. An open branch in a completed tableaux guarantees the existence of an Kripke model in which the formula is not valid; hence it is not a theorem of Gelfand Logic.     

An analytic tableau calculus for a temporalised belief logic

A tableau is a refutation-based decision procedure for a related logic, and is among the most popular proof procedures for modal logics. In this paper, we present a labelled tableau calculus for a temporalised belief logic called TML⁺, which is obtained by adding a linear-time temporal logic onto a belief logic by the temporalisation method of Finger and Gabbay. We first establish the soundness and the completeness of the labelled tableau calculus based on the soundness and completeness results of its constituent logics. We then sketch a resolution-type proof procedure that complements the tableau calculus and also propose a model checking algorithm for TML⁺ based on the recent results for model checking procedures for temporalised logics. TML⁺ is suitable for formalising trust and agent beliefs and reasoning about their evolution for agent-based systems. Based on the logic TML⁺, the proposed labelled tableau calculus could be used for analysis, design and verification of agent-based systems operating in dynamic environments.     

Analytic Tableau Systems and Interpolation for the Modal Logics KB, KDB, K5, KD5

We give complete sequent-like tableau systems for the modal logics KB, KDB, K5, and KD5. Analytic cut rules are used to obtain the completeness. Our systems have the analytic superformula property and can thus give a decision procedure. Using the systems, we prove the Craig interpolation lemma for the mentioned logics.     

Commodious Axiomatization of Quantifiers in Multiple-Valued Logic

We provide tools for a concise axiomatization of a broad class of quantifiers in many-valued logic, so-called distribution quantifiers. Although sound and complete axiomatizations for such quantifiers exist, their size renders them virtually useless for practical purposes. We show that for quantifiers based on finite distributive lattices compact axiomatizations can be obtained schematically. This is achieved by providing a link between skolemized signed formulas and filters/ideals in Boolean set lattices. Then lattice theoretic tools such as Birkhoff's representation theorem for finite distributive lattices are used to derive tableau-style axiomatizations of distribution quantifiers.     

Reasoning about conscious experience with axiomatic and graphical mathematics

We cast aspects of consciousness in axiomatic mathematical terms, using the graphical calculus of general process theories (a.k.a symmetric monoidal categories and Frobenius algebras therein). This calculus exploits the ontological neutrality of process theories. A toy example using the axiomatic calculus is given to show the power of this approach, recovering other aspects of conscious experience, such as external and internal subjective distinction, privacy or unreadability of personal subjective experience, and phenomenal unity, one of the main issues for scientific studies of consciousness. In fact, these features naturally arise from the compositional nature of axiomatic calculus.     

Rough Sets and 3-Valued Logics

In the paper we explore the idea of describing Pawlak’s rough sets using three-valued logic, whereby the value t corresponds to the positive region of a set, the value f — to the negative region, and the undefined value u — to the border of the set. Due to the properties of the above regions in rough set theory, the semantics of the logic is described using a non-deterministic matrix (Nmatrix). With the strong semantics, where only the value t is treated as designated, the above logic is a “common denominator” for Kleene and Łukasiewicz 3-valued logics, which represent its two different “determinizations”. In turn, the weak semantics—where both t and u are treated as designated—represents such a “common denominator” for two major 3-valued paraconsistent logics. We give sound and complete, cut-free sequent calculi for both versions of the logic generated by the rough set Nmatrix. Then we derive from these calculi sequent calculi with the same properties for the various “determinizations” of those two versions of the logic (including Łukasiewicz 3-valued logic). Finally, we show how to embed the four above-mentioned determinizations in extensions of the basic rough set logics obtained by adding to those logics a special two-valued “definedness” or “crispness” operator.     

Connection Tableau Calculi with Disjunctive Constraints

Automated theorem proving amounts to solving search problems in usually tremendous search spaces. A lot of research therefore focuses on search space reductions. Our approach reduces the search space which arises when using so-called connection tableau calculi for first-order automated theorem proving. It uses disjunctive constraints over first-order equations to compress certain parts of this search space. We present the basics of our constrained-connection-tableau calculi, a constraint extension of connection tableau calculi, and deal with the efficient handling of constraints during the search process. The new techniques are integrated into the automated connection tableau prover Setheo.     

How True It Is = Who Says It’s True

This is a largely expository paper in which the following simple idea is pursued. Take the truth value of a formula to be the set of agents that accept the formula as true. This means we work with an arbitrary (finite) Boolean algebra as the truth value space. When this is properly formalized, complete modal tableau systems exist, and there are natural versions of bisimulations that behave well from an algebraic point of view. There remain significant problems concerning the proper formalization, in this context, of natural language statements, particularly those involving negative knowledge and common knowledge. A case study is presented which brings these problems to the fore. None of the basic material presented here is new to this paper—all has appeared in several papers over many years, by the present author and by others. Much of the development in the literature is more general than here—we have confined things to the Boolean case for simplicity and clarity. Most proofs are omitted, but several of the examples are new. The main virtue of the present paper is its coherent presentation of a systematic point of view—identify the truth value of a formula with the set of those who say the formula is true.