Actuality in Propositional Modal Logic

We show that the actuality operator A is redundant in any propositional modal logic characterized by a class of Kripke models (respectively, neighborhood models). Specifically, we prove that for every formula ${\phi}$ in the propositional modal language with A, there is a formula ${\psi}$ not containing A such that ${\phi}$ and ${\psi}$ are materially equivalent at the actual world in every Kripke model (respectively, neighborhood model). Inspection of the proofs leads to corresponding proof-theoretic results concerning the eliminability of the actuality operator in the actuality extension of any normal propositional modal logic and of any “classical” modal logic. As an application, we provide an alternative proof of a result of Williamson’s to the effect that the compound operator A□ behaves, in any normal logic between T and S5, like the simple necessity operator □ in S5.     

Inverse Images of Box Formulas in Modal Logic

We investigate, for several modal logics but concentrating on KT, KD45, S4 and S5, the set of formulas B for which ${\square B}$ is provably equivalent to ${\square A}$ for a selected formula A (such as p, a sentence letter). In the exceptional case in which a modal logic is closed under the (‘cancellation’) rule taking us from ${\square C \leftrightarrow \square D}$ to ${C \leftrightarrow D}$ , there is only one formula B, to within equivalence, in this inverse image, as we shall call it, of ${\square A}$ (relative to the logic concerned); for logics for which the intended reading of “ ${\square}$ ” is epistemic or doxastic, failure to be closed under this rule indicates that from the proposition expressed by a knowledge- or belief-attribution, the propositional object of the attitude in question cannot be recovered: arguably, a somewhat disconcerting situation. More generally, the inverse image of ${\square A}$ may comprise a range of non-equivalent formulas, all those provably implied by one fixed formula and provably implying another—though we shall see that for several choices of logic and of the formula A, there is not even such an ‘interval characterization’ of the inverse image (of ${\square A}$ ) to be found.     

The variance of d′ estimates obtained in yes—no and two-interval forced choice procedures

In studies of detection and discrimination, data are often obtained in the form of a 2 × 2 matrix and then converted to an estimate of d′, based on the assumptions that the underlying decision distributions are Gaussian and equal in variance. The statistical properties of the estimate of d′, $\hat d'$ , are well understood for data obtained using the yes—no procedure, but less effort has been devoted to the more commonly used two-interval forced choice (2IFC) procedure. The variance associated with $\hat d'$ is a function of trued′ in both procedures, but for small values of trued′, the variance of $\hat d'$ obtained using the 2IFC procedure is predicted to be less than the variance of $\hat d'$ obtained using yes—no; for large values of trued′, the variance of $\hat d'$ obtained using the 2IFC procedure is predicted to be greater than the variance of $\hat d'$ from yes—no. These results follow from standard assumptions about the relationship between the two procedures. The present paper reviews the statistical properties of $\hat d'$ obtained using the two standard procedures and compares estimates of the variance of $\hat d'$ as a function of trued′ with the variance observed in values of $\hat d'$ obtained with a 2IFC procedure.     

What is Nominalistic Mereology?

Hybrid languages are introduced in order to evaluate the strength of “minimal” mereologies with relatively strong frame definability properties. Appealing to a robust form of nominalism, I claim that one investigated language $\mathcal {H}_{\textsf {m}}$ is maximally acceptable for nominalistic mereology. In an extension $\mathcal {H}_{\textsf {gem}}$ of $\mathcal {H}_{\textsf {m}}$ , a modal analog for the classical systems of Leonard and Goodman (J Symb Log 5:45–55, 1940) and Le?niewski (1916) is introduced and shown to be complete with respect to 0-deleted Boolean algebras. We characterize the formulas of first-order logic invariant for $\mathcal {H}_{\textsf {gem}}$ -bisimulations.     

Dynamic Modalities

A new modal logic containing four dynamic modalities with the following informal reading is introduced: ${\square^\forall}$ – always necessary, ${\square^\exists}$ – sometimes necessary, and their duals – ${\diamondsuit^\forall}$ – always possibly, and ${\diamondsuit^\exists}$ – sometimes possibly. We present a complete axiomatization with respect to the intended formal semantics and prove decidability via fmp.     

On the Dynamic Logic of Agency and Action

We present a Hilbert style axiomatization and an equational theory for reasoning about actions and capabilities. We introduce two novel features in the language of propositional dynamic logic, converse as backwards modality and abstract processes specified by preconditions and effects, written as ${\varphi \Rightarrow \psi}$ and first explored in our recent paper (Hartonas, Log J IGPL Oxf Univ Press, 2012), where a Gentzen-style sequent calculus was introduced. The system has two very natural interpretations, one based on the familiar relational semantics and the other based on type semantics, where action terms are interpreted as types of actions (sets of binary relations). We show that the proof systems do not distinguish between the two kinds of semantics, by completeness arguments. Converse as backwards modality together with action types allow us to produce a new purely equational axiomatization of Dynamic Algebras, where iteration is axiomatized independently of box and where the fixpoint and Segerberg induction axioms are derivable. The system also includes capabilities operators and our results provide then a finitary Hilbert-style axiomatization and a decidable system for reasoning about agent capabilities, missing in the KARO framework.     

On Birkhoff’s Common Abstraction Problem

In his milestone textbook Lattice Theory, Garrett Birkhoff challenged his readers to develop a ??common abstraction?? that includes Boolean algebras and latticeordered groups as special cases. In this paper, after reviewing the past attempts to solve the problem, we provide our own answer by selecting as common generalization of ${\mathcal{B} \mathcal{A}}$ and ${\mathcal{L} \mathcal{G}}$ their join ${\mathcal{B} \mathcal{A} \vee \mathcal{L} \mathcal{G}}$ in the lattice of subvarieties of ${\mathcal{F} \mathcal{L}}$ (the variety of FL-algebras); we argue that such a solution is optimal under several respects and we give an explicit equational basis for ${\mathcal{B} \mathcal{A} \vee \mathcal{L} \mathcal{G}}$ relative to ${\mathcal{F} \mathcal{L}}$ . Finally, we prove a Holland-type representation theorem for a variety of FL-algebras containing ${\mathcal{B} \mathcal{A} \vee \mathcal{L} \mathcal{G}}$ .     

Decidability of the Equational Theory of the Continuous Geometry CG(\Bbb {F})

For $\Bbb {F}$ the field of real or complex numbers, let $CG(\Bbb {F})$ be the continuous geometry constructed by von Neumann as a limit of finite dimensional projective geometries over $\Bbb {F}$ . Our purpose here is to show the equational theory of $CG(\Bbb {F})$ is decidable.     

Reconstructing an Open Order from Its Closure, with Applications to Space-Time Physics and to Logic

In his logical papers, Leo Esakia studied corresponding ordered topological spaces and order-preserving mappings. Similar spaces and mappings appear in many other application areas such the analysis of causality in space-time. It is known that under reasonable conditions, both the topology and the original order relation ${\preccurlyeq}$ can be uniquely reconstructed if we know the “interior” ${\prec}$ of the order relation. It is also known that in some cases, we can uniquely reconstruct ${\prec}$ (and hence, topology) from ${\preccurlyeq}$ . In this paper, we show that, in general, under reasonable conditions, the open order ${\prec}$ (and hence, the corresponding topology) can be uniquely determined from its closure ${\preccurlyeq}$ .     

From constants to consequence, and back

Bolzano??s definition of consequence in effect associates with each set X of symbols (in a given interpreted language) a consequence relation ${\Rightarrow_X}$ . We present this in a precise and abstract form, in particular studying minimal sets of symbols generating ${\Rightarrow_X}$ . Then we present a method for going in the other direction: extracting from an arbitrary consequence relation ${\Rightarrow}$ its associated set ${C_\Rightarrow}$ of constants. We show that this returns the expected logical constants from familiar consequence relations, and that, restricting attention to sets of symbols satisfying a strong minimality condition, there is an isomorphism between the set of strongly minimal sets of symbols and the set of corresponding consequence relations (both ordered under inclusion).     

Dependence and Independence

We introduce an atomic formula ${\vec{y} \bot_{\vec{x}}\vec{z}}$ intuitively saying that the variables ${\vec{y}}$ are independent from the variables ${\vec{z}}$ if the variables ${\vec{x}}$ are kept constant. We contrast this with dependence logic ${\mathcal{D}}$ based on the atomic formula = ${(\vec{x}, \vec{y})}$ , actually equivalent to ${\vec{y} \bot_{\vec{x}}\vec{y}}$ , saying that the variables ${\vec{y}}$ are totally determined by the variables ${\vec{x}}$ . We show that ${\vec{y} \bot_{\vec{x}}\vec{z}}$ gives rise to a natural logic capable of formalizing basic intuitions about independence and dependence. We show that ${\vec{y} \bot_{\vec{x}}\vec{z}}$ can be used to give partially ordered quantifiers and IF-logic an alternative interpretation without some of the shortcomings related to so called signaling that interpretations using = ${(\vec{x}, \vec{y})}$ have.     

Semi-intuitionistic Logic

The purpose of this paper is to define a new logic ${\mathcal {SI}}$ called semi-intuitionistic logic such that the semi-Heyting algebras introduced in [4] by Sankappanavar are the semantics for ${\mathcal {SI}}$ . Besides, the intuitionistic logic will be an axiomatic extension of ${\mathcal {SI}}$ .     

Decidability of General Extensional Mereology

The signature of the formal language of mereology contains only one binary predicate P which stands for the relation “being a part of”. Traditionally, P must be a partial ordering, that is, ${\forall{x}Pxx, \forall{x}\forall{y}((Pxy\land Pyx)\to x=y)}$ and ${\forall{x}\forall{y}\forall{z}((Pxy\land Pyz)\to Pxz))}$ are three basic mereological axioms. The best-known mereological theory is “general extensional mereology”, which is axiomatized by the three basic axioms plus the following axiom and axiom schema: (Strong Supplementation) ${\forall{x}\forall{y}(\neg Pyx\to \exists z(Pzy\land \neg Ozx))}$ , where Oxy means ${\exists z(Pzx\land Pzy)}$ , and (Fusion) ${\exists x\alpha \to \exists z\forall y(Oyz\leftrightarrow \exists x(\alpha \land Oyx))}$ , for any formula α where z and y do not occur free. In this paper, I will show that general extensional mereology is decidable, and will also point out that the decidability of the first-order approximation of the theory of complete Boolean algebras can be shown in the same way.     

On Endomorphisms of Ockham Algebras with Pseudocomplementation

A pO-algebra ${(L; f, \, ^{\star})}$ is an algebra in which (L; f) is an Ockham algebra, ${(L; \, ^{\star})}$ is a p-algebra, and the unary operations f and ${^{\star}}$ commute. Here we consider the endomorphism monoid of such an algebra. If ${(L; f, \, ^{\star})}$ is a subdirectly irreducible pK _1,1- algebra then every endomorphism ${\vartheta}$ is a monomorphism or ${\vartheta^3 = \vartheta}$ . When L is finite the endomorphism monoid of L is regular, and we determine precisely when it is a Clifford monoid.     

Information closure and the sceptical objection

In this article, I define and then defend the principle of information closure (pic) against a sceptical objection similar to the one discussed by Dretske in relation to the principle of epistemic closure. If I am successful, given that pic is equivalent to the axiom of distribution and that the latter is one of the conditions that discriminate between normal and non-normal modal logics, a main result of such a defence is that one potentially good reason to look for a formalization of the logic of “ $S$ is informed that $p$ ” among the non-normal modal logics, which reject the axiom, is also removed. This is not to argue that the logic of “ $S$ is informed that $p$ ” should be a normal modal logic, but that it could still be insofar as the objection that it could not be, based on the sceptical objection against pic, has been removed. In other word, I shall argue that the sceptical objection against pic fails, so such an objection provides no ground to abandon the normal modal logic B (also known as KTB) as a formalization of “ $S$ is informed that $p$ ”, which remains plausible insofar as this specific obstacle is concerned.     

The Church–Fitch knowability paradox in the light of structural proof theory

Anti-realist epistemic conceptions of truth imply what is called the knowability principle: All truths are possibly known. The principle can be formalized in a bimodal propositional logic, with an alethic modality ${\diamondsuit}$ and an epistemic modality ${\mathcal{K}}$ , by the axiom scheme ${A \supset \diamondsuit \mathcal{K} A}$ (KP). The use of classical logic and minimal assumptions about the two modalities lead to the paradoxical conclusion that all truths are known, ${A \supset \mathcal{K} A}$ (OP). A Gentzen-style reconstruction of the Church–Fitch paradox is presented following a labelled approach to sequent calculi. First, a cut-free system for classical (resp. intuitionistic) bimodal logic is introduced as the logical basis for the Church–Fitch paradox and the relationships between ${\mathcal {K}}$ and ${\diamondsuit}$ are taken into account. Afterwards, by exploiting the structural properties of the system, in particular cut elimination, the semantic frame conditions that correspond to KP are determined and added in the form of a block of nonlogical inference rules. Within this new system for classical and intuitionistic “knowability logic”, it is possible to give a satisfactory cut-free reconstruction of the Church–Fitch derivation and to confirm that OP is only classically derivable, but neither intuitionistically derivable nor intuitionistically admissible. Finally, it is shown that in classical knowability logic, the Church–Fitch derivation is nothing else but a fallacy and does not represent a real threat for anti-realism.     

On the Algebraizability of the Implicational Fragment of Abelian Logic

In this paper we consider the implicational fragment of Abelian logic \({{{\sf A}_{\rightarrow}}}\) . We show that although the Abelian groups provide an semantics for the set of theorems of \({{{\sf A}_{\rightarrow}}}\) they do not for the associated consequence relation. We then show that the consequence relation is not algebraizable in the sense of Blok and Pigozzi (Mem Am Math Soc 77, 1989). In the second part of the paper, we investigate an extension of \({{{\sf A}_{\rightarrow}}}\) in the same language and having the same set of theorems and show that this new consequence relation is algebraizable with the Abelian groups as its equivalent algebraic semantics. Finally, we show that although \({{{\sf A}_{\rightarrow}}}\) is not algebraizable, it is order-algebraizable in the sense of Raftery (Ann Pure Appl Log 164:251–283, 2013).     

IF Modal Logic and Classical Negation

The present paper provides novel results on the model theory of Independence friendly modal logic. We concentrate on its particularly well-behaved fragment that was introduced in Tulenheimo and Sevenster (Advances in Modal Logic, 2006). Here we refer to this fragment as ‘Simple IF modal logic’ (IFML _s ). A model-theoretic criterion is presented which serves to tell when a formula of IFML _s is not equivalent to any formula of basic modal logic (ML). We generalize the notion of bisimulation familiar from ML; the resulting asymmetric simulation concept is used to prove that IFML _s is not closed under complementation. In fact we obtain a much stronger result: the only IFML _s formulas admitting their classical negation to be expressed in IFML _s itself are those whose truth-condition is in fact expressible in ML.