Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics

We establish a generic upper bound ExpTime for reasoning with global assumptions (also known as TBoxes) in coalgebraic modal logics. Unlike earlier results of this kind, our bound does not require a tractable set of tableau rules for the instance logics, so that the result applies to wider classes of logics. Examples are Presburger modal logic, which extends graded modal logic with linear inequalities over numbers of successors, and probabilistic modal logic with polynomial inequalities over probabilities. We establish the theoretical upper bound using a type elimination algorithm. We also provide a global caching algorithm that potentially avoids building the entire exponential-sized space of candidate states, and thus offers a basis for practical reasoning. This algorithm still involves frequent fixpoint computations; we show how these can be handled efficiently in a concrete algorithm modelled on Liu and Smolka’s linear-time fixpoint algorithm. Finally, we show that the upper complexity bound is preserved under adding nominals to the logic, i.e., in coalgebraic hybrid logic.

Counterparts, Essences and Quantified Modal Logic

It is commonplace to formalize propositions involving essential properties of objects in a language containing modal operators and quantifiers. Assuming David Lewis’s counterpart theory as a semantic framework for quantified modal logic, I will show that certain statements discussed in the metaphysics of modality de re, such as the sufficiency condition for essential properties, cannot be faithfully formalized. A natural modification of Lewis’s translation scheme seems to be an obvious solution but is not acceptable for various reasons. Consequently, the only safe way to express some intuitions regarding essential properties is to use directly the language of counterpart theory without modal operators.

On Formalizing Logical Modalities

This paper is in the scope of the philosophy of modal logic; more precisely, it concerns the semantics of modal logic, when the modal elements are interpreted as logical modalities. Most authors have thought that the logic for logical modality—that is, the one to be used to formalize the notion of logical truth (and other related notions)—is to be found among logical systems in which modalities are allowed to be iterated. This has raised the problem of the adequacy, to that formalization purpose, of some modal schemes, such as S4 and S5 . It has been argued that the acceptance of S5 leads to non-normal modal systems, in which the uniform substitution rule fails. The thesis supported in this paper is that such a failure is rather to be attributed to what will be called “Condition of internalization.” If this is correct, there seems to be no normal modal logic system capable of formalizing logical modality, even when S5 is rejected in favor of a weaker system such as S4, as recently proposed by McKeon.

Expressive Logics for Coinductive Predicates

The classical Hennessy-Milner theorem says that two states of an image-finite transition system are bisimilar if and only if they satisfy the same formulas in a certain modal logic. In this paper we study this type of result in a general context, moving from transition systems to coalgebras and from bisimilarity to coinductive predicates. We formulate when a logic fully characterises a coinductive predicate on coalgebras, by providing suitable notions of adequacy and expressivity, and give sufficient conditions on the semantics. The approach is illustrated with logics characterising similarity, divergence and a behavioural metric on automata.

The Evil That Free Will Does: Plantinga’s Dubious Defense

Alvin Plantinga’s controversial free will defense (FWD) for the problem of evil is an important attempt to show with certainty that moral evils are compatible and justifiable with God’s omnipotence and omniscience. I agree with critics who argue that it is untenable and the FWD fails. This paper proposes new criticisms by analyzing Plantinga’s presuppositions and objectionable assumptions in God, Freedom and Evil. Notably, his limited concept of omnipotence, and possible worlds theory lack rigorous argument and are subjectively biased with irrelevant weak examples. My ontological possible worlds theory (Possible Conditional Timelines) shows that it is very likely that the omnipotent God exists of necessity in some worlds but perhaps not this one. Omnipotence is total and absolute, and should imply the freedom of will to actualize all worlds God chooses. Plantinga’s position regarding God’s omniscience of future counterfactuals is implausible based on modal logic conjecture.

Using Transition Systems to Formalise Ideas from Vedanta

Vedanta is one of the oldest philosophical systems. While there are many detailed commentaries on Vedanta, there are very few mathematical descriptions of the different concepts developed there. This article shows how ideas from theoretical computer science can be used to explain Vedanta. The standard idea of transition systems and modal logic are used to develop a formal description for the different ideas in Vedanta. The generality of the formalism is illustrated via a number of examples including \samsara, \Patanjali's yoga sutras, karma, the three avasthas from the Mandukya Upanishad and the key difference between advaita and dvaita in relation to moksha.

A. N. PRIOR’S SYSTEM Q: A REVIEW

In his “Time and Modality”, based on his own philosophical motivations, Arthur Norman Prior proposed the modal logic Q as a correct modal logic in 1957. Prior developed Q in order to offer a logic for contingent beings, in which one could rationally state that some beings are contingent and some are necessary. One may say that Q is an actualist modal logic with a natural semantics. This review article is a developed description/discussion of/on “The System Q” that is the fifth chapter of “Time and Modality”. I have attempted to analyse the logical structure of system Q in order to provide a more understandable description as well as logical analysis for today’s logicians, philosophers, and information-computer scientists. In the paper, the Polish notations are translated into modern notations in order to be more comprehensible and to support the developed formal descriptions and semantic analysis.