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.     

Complexity Results of STIT Fragments

We provide a Kripke semantics for a STIT logic with the ??next?? operator. As the atemporal group STIT is undecidable and unaxiomatizable, we are interested in strict fragments of atemporal group STIT. First we prove that the satisfiability problem of a formula of the fragment made up of individual coalitions plus the grand coalition is also NEXPTIME-complete. We then generalize this result to a fragment where coalitions are in a given lattice. We also prove that if we restrict the language to nested coalitions the satisfiability problem is NP-complete if the number of agents is fixed and PSPACEcomplete if the number of agents is variable. Finally we embed individual STIT with the ??next?? operator into a fragment of atemporal group STIT.     

Extensions of Priest-da Costa Logic

In this paper, we look at applying the techniques from analyzing superintuitionistic logics to extensions of the cointuitionistic Priest-da Costa logic daC (introduced by Graham Priest as “da Costa logic”). The relationship between the superintuitionistic axioms- definable in daC- and extensions of Priest-da Costa logic (sdc-logics) is analyzed and applied to exploring the gap between the maximal si-logic SmL and classical logic in the class of sdc-logics. A sequence of strengthenings of Priest-da Costa logic is examined and employed to pinpoint the maximal non-classical extension of both daC and Heyting-Brouwer logic HB . Finally, the relationship between daC and Logics of Formal Inconsistency is examined.     

Dynamics of lying

We propose a dynamic logic of lying, wherein a ‘lie that $\varphi $ ’ (where $\varphi $ is a formula in the logic) is an action in the sense of dynamic modal logic, that is interpreted as a state transformer relative to the formula $\varphi $ . The states that are being transformed are pointed Kripke models encoding the uncertainty of agents about their beliefs. Lies can be about factual propositions but also about modal formulas, such as the beliefs of other agents or the belief consequences of the lies of other agents. We distinguish two speaker perspectives: (Obs) an outside observer who is lying to an agent that is modelled in the system, and (Ag) an agent who is lying to another agent, and where both are modelled in the system. We distinguish three addressee perspectives: (Cred) the credulous agent who believes everything that it is told (even at the price of inconsistency), (Skep) the skeptical agent who only believes what it is told if that is consistent with its current beliefs, and (Rev) the belief revising agent who believes everything that it is told by consistently revising its current, possibly conflicting, beliefs. The logics have complete axiomatizations, which can most elegantly be shown by way of their embedding in what is known as action model logic or in the extension of that logic to belief revision.     

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.     

Reasoning About Games

A mixture of propositional dynamic logic and epistemic logic that we call PDL + E is used to give a formalization of Artemov??s knowledge based reasoning approach to game theory, (KBR), [4, 5]. Epistemic states of players are represented explicitly and reasoned about formally. We give a detailed analysis of the Centipede game using both proof theoretic and semantic machinery. This helps make the case that PDL + E can be a useful basis for the logical investigation of game theory.     

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.     

Fatal Heyting Algebras and Forcing Persistent Sentences

Hamkins and L?we proved that the modal logic of forcing is S4.2. In this paper, we consider its modal companion, the intermediate logic KC and relate it to the fatal Heyting algebra H _ZFC of forcing persistent sentences. This Heyting algebra is equationally generic for the class of fatal Heyting algebras. Motivated by these results, we further analyse the class of fatal Heyting algebras.     

Finite axiomatization for some intermediate logics

LetN. be the set of all natural numbers (except zero), and letD _n ^* = {k ∈N ∶k|n} ∪ {0} wherek¦n if and only ifn=k.x f or somex∈N. Then, an ordered setD _n ^* = 〈D _n ^* , ? _n , wherex? _ny iffx¦y for anyx, y∈D _n ^* , can easily be seen to be a pseudo-boolean algebra. In [5], V.A. Jankov has proved that the class of algebras {D _n ^* ∶n∈B}, whereB =,{k ∈N∶ ? \(\mathop \exists \limits_{n \in N} \) (n > 1 ≧n ² k)is finitely axiomatizable. The present paper aims at showing that the class of all algebras {D _n ^* ∶n∈B} is also finitely axiomatizable. First, we prove that an intermediate logic defined as follows: $$LD = Cn(INT \cup \{ p_3 \vee [p_3 \to (p_1 \to p_2 ) \vee (p_2 \to p_1 )]\} )$$ finitely approximatizable. Then, defining, after Kripke, a model as a non-empty ordered setH = 〈K, ?〉, and making use of the set of formulas true in this model, we show that any finite strongly compact pseudo-boolean algebra ? is identical with. the set of formulas true in the Kripke modelH _B = 〈P(?), ?〉 (whereP(?) stands for the family of all prime filters in the algebra ?). Furthermore, the concept of a structure of divisors is defined, and the structure is shown to beH D _n ^* = 〈P (D _n ^* ), ?〉for anyn∈N. Finally, it is proved that for any strongly compact pseudo-boolean algebraU satisfying the axiomp ₃∨ [p ₃→(p₁→p₂)∨(p₂→p₁)] there is a structure of divisorsD _* ⁿ such that it is possible to define a strong homomorphism froomiH D _n ^* ontoH D _U . Exploiting, among others, this property, it turns out to be relatively easy to show that \(LD = \mathop \cap \limits_{n \in N} E(\mathfrak{D}_n^* )\) .     

An Inconsistency-Adaptive Deontic Logic for Normative Conflicts

We present the inconsistency-adaptive deontic logic DP ^r , a nonmonotonic logic for dealing with conflicts between normative statements. On the one hand, this logic does not lead to explosion in view of normative conflicts such as O A?∧?O ～A, O A?∧?P ～A or even O A?∧?～O A. On the other hand, DP ^r still verifies all intuitively reliable inferences valid in Standard Deontic Logic (SDL). DP ^r interprets a given premise set ‘as normally as possible’ with respect to SDL. Whereas some SDL-rules are verified unconditionally by DP ^r , others are verified conditionally. The latter are applicable unless they rely on formulas that turn out to behave inconsistently in view of the premises. This dynamic process is mirrored by the proof theory of DP ^r .     

On the axiomatization of finiteK-frames

We find a short way to construct a formula which axiomatizes a given finite frame of the modal logicK, in the sense that for each finite frameA, we construct a formula ωA which holds in those and only those frames in which every formula true inA holds. To obtain this result we find, for each finite model \(\mathfrak{A}\) and each natural numbern, a formula ω \(\mathfrak{A}\) which holds in those and only those models in which every formula true in \(\mathfrak{A}\) , and involving the firstn propositional letters, holds.     

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.     

Propositional Epistemic Logics with Quantification Over Agents of Knowledge

The paper presents a family of propositional epistemic logics such that languages of these logics are extended by quantification over modal (epistemic) operators or over agents of knowledge and extended by predicate symbols that take modal (epistemic) operators (or agents) as arguments. Denote this family by \({\mathcal {P}\mathcal {E}\mathcal {L}}_{({ QK})}\). There exist epistemic logics whose languages have the above mentioned properties (see, for example Corsi and Orlandelli in Stud Log 101:1159–1183, 2013; Fitting et al. in Stud Log 69:133–169, 2001; Grove in Artif Intell 74(2):311–350, 1995; Lomuscio and Colombetti in Proceedings of ATAL 1996. Lecture Notes in Computer Science (LNCS), vol 1193, pp 71–85, 1996). But these logics are obtained from first-order modal logics, while a logic of \({\mathcal {P}\mathcal {E}\mathcal {L}}_{({ QK})}\) can be regarded as a propositional multi-modal logic whose language includes quantifiers over modal (epistemic) operators and predicate symbols that take modal (epistemic) operators as arguments. Among the logics of \({\mathcal {P}\mathcal {E}\mathcal {L}}_{({ QK})}\) there are logics with a syntactical distinction between two readings of epistemic sentences: de dicto and de re (between ‘knowing that’ and ‘knowing of’). We show the decidability of logics of \({\mathcal {P}\mathcal {E}\mathcal {L}}_{({ QK})}\) with the help of the loosely guarded fragment (LGF) of first-order logic. Namely, we generalize LGF to a higher-order decidable loosely guarded fragment. The latter fragment allows us to construct various decidable propositional epistemic logics with quantification over modal (epistemic) operators. The family of this logics coincides with \({\mathcal {P}\mathcal {E}\mathcal {L}}_{({ QK})}\). There are decidable propositional logics such that these logics implicitly contain quantification over agents of knowledge, but languages of these logics are usual propositional epistemic languages without quantifiers and predicate symbols (see Grove and Halpern in J Log Comput 3(4):345–378, 1993). Some logics of \({\mathcal {P}\mathcal {E}\mathcal {L}}_{({ QK})}\) can be regarded as counterparts of logics defined in Grove and Halpern (J Log Comput 3(4):345–378, 1993). We prove that the satisfiability problem for these logics of \({\mathcal {P}\mathcal {E}\mathcal {L}}_{({ QK})}\) is Pspace-complete using their counterparts in Grove and Halpern (J Log Comput 3(4):345–378, 1993).     

Further evidence for phonological constraints on visual lexical access: TOWED primes FROG

If the phonological codes of visually presented words are assembled-rapidly and automatically for use in lexical access, then words that sound alike should induce similar activity within the internal lexicon.Towed is homophonous with TOAD, which is semantically related tofrog, andbeach is homophonous withbeech, which is semantically related totree. Stimuli such as these were used in a priming-of-namingtask, in which words homophonous with associates of the target words preceded the targets at an onset asynchrony of 100 msec. Relative to spelling controls (trod, bench), the low-frequencytowed and the high-frequencybeach speeded up the naming offrog andtree, respectively, to the same degree. This result was discussed in relation to the accumulating evidence for the primacy of phonological constraints in visual lexical access. nt]mis|This research was supported in part by National Institute of Child Health and Human Development Grants HD-08945 and HD-0 1994 to the first author and Haskins Laboratories, respectively.     

Arithmetical Completeness Theorem for Modal Logic $$\mathsf{}$$

We prove that for any recursively axiomatized consistent extension T of Peano Arithmetic, there exists a \(\Sigma _2\) provability predicate of T whose provability logic is precisely the modal logic \(\mathsf{K}\). For this purpose, we introduce a new bimodal logic \(\mathsf{GLK}\), and prove the Kripke completeness theorem and the uniform arithmetical completeness theorem for \(\mathsf{GLK}\).     

Best Unifiers in Transitive Modal Logics

This paper offers a brief analysis of the unification problem in modal transitive logics related to the logic S4: S4 itself, K4, Grz and Gödel-Löb provability logic GL. As a result, new, but not the first, algorithms for the construction of ??best?? unifiers in these logics are being proposed. The proposed algorithms are based on our earlier approach to solve in an algorithmic way the admissibility problem of inference rules for S4 and Grz. The first algorithms for the construction of ??best?? unifiers in the above mentioned logics have been given by S. Ghilardi in [16]. Both the algorithms in [16] and ours are not much computationally efficient. They have, however, an obvious significant theoretical value a portion of which seems to be the fact that they stem from two different methodological approaches.     

Importing Logics

The novel notion of importing logics is introduced, subsuming as special cases several kinds of asymmetric combination mechanisms, like temporalization [8, 9], modalization [7] and exogenous enrichment [13, 5, 12, 4, 1]. The graph-theoretic approach proposed in [15] is used, but formulas are identified with irreducible paths in the signature multi-graph instead of equivalence classes of such paths, facilitating proofs involving inductions on formulas. Importing is proved to be strongly conservative. Conservative results follow as corollaries for temporalization, modalization and exogenous enrichment.     

Completeness in Hybrid Type Theory

We show that basic hybridization (adding nominals and @ operators) makes it possible to give straightforward Henkin-style completeness proofs even when the modal logic being hybridized is higher-order. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret \(@_i\) in propositional and first-order hybrid logic. This means: interpret \(@_i\alpha _a\) , where \(\alpha _a\) is an expression of any type \(a\) , as an expression of type \(a\) that rigidly returns the value that \(\alpha_a\) receives at the i-world. The axiomatization and completeness proofs are generalizations of those found in propositional and first-order hybrid logic, and (as is usual inhybrid logic) we automatically obtain a wide range of completeness results for stronger logics and languages. Our approach is deliberately low-tech. We don’t, for example, make use of Montague’s intensional type s, or Fitting-style intensional models; we build, as simply as we can, hybrid logicover Henkin’s logic.     

Arithmetical Soundness and Completeness for $$\varvec{\Sigma }_{\varvec{2}}$$ Numerations

We prove that for each recursively axiomatized consistent extension T of Peano Arithmetic and \(n \ge 2\), there exists a \(\Sigma _2\) numeration \(\tau (u)\) of T such that the provability logic of the provability predicate \(\mathsf{Pr}_\tau (x)\) naturally constructed from \(\tau (u)\) is exactly \(\mathsf{K}+ \Box (\Box ^n p \rightarrow p) \rightarrow \Box p\). This settles Sacchetti’s problem affirmatively.