We present a new notion of game equivalence that captures basic powers of interacting players. We provide a representation theorem, a complete logic, and a new game algebra for basic powers. In doing so, we establish connections with imperfect information games and epistemic logic. We also identify some new open problems concerning logic and games.

This paper explores a new language of neighbourhood structures where existential information can be given about what kind of worlds occur in a neighbourhood of a current world. The resulting system of ‘instantial neighbourhood logic’ INL has a nontrivial mix of features from relational semantics and from neighbourhood semantics. We explore some basic model-theoretic behavior, including a matching notion of bisimulation, and give a complete axiom system for which we prove completeness by a new normal form technique. In addition, we (...) relate INL to other modal logics by means of translations, and determine its precise SAT complexity. Finally, we discuss proof-theoretic fine-structure of INL in terms of semantic tableaux and some expressive fine-structure in terms of fragments, while discussing concrete illustrations of the instantial neighborhood language in topological spaces, in games with powers for players construed in a new way, as well as in dynamic logics of acquiring or deleting evidence. We conclude with some coalgebraic perspectives on what is achieved in this paper. Many of these final themes suggest follow-up work of independent interest. (shrink)

The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.

We propose a new perspective on logics of computation by combining instantial neighborhood logic \ with bisimulation safe operations adapted from \. \ is a recent modal logic, based on an extended neighborhood semantics which permits quantification over individual neighborhoods plus their contents. This system has a natural interpretation as a logic of computation in open systems. Motivated by this interpretation, we show that a number of familiar program constructors can be adapted to instantial neighborhood semantics to preserve invariance for (...) instantial neighborhood bisimulations, the appropriate bisimulation concept for \. We also prove that our extended logic \ is a conservative extension of dual-free game logic, and its semantics generalizes the monotone neighborhood semantics of game logic. Finally, we provide a sound and complete system of axioms for \, and establish its finite model property and decidability. (shrink)

We investigate sequent calculi for the weak modal (propositional) system reduced to the equivalence rule and extensions of it up to the full Kripke system containing monotonicity, conjunction and necessitation rules. The calculi have cut elimination and we concentrate on the inversion of rules to give in each case an effective procedure which for every sequent either furnishes a proof or a finite countermodel of it. Applications to the cardinality of countermodels, the inversion of rules and the derivability of Löb (...) rules are given. (shrink)

This paper develops sequent calculi for several classical modal logics. Utilizing a polymodal translation of the standard modal language, we are able to establish a base system for the minimal classical modal logic E from which we generate extensions in a modular manner. Our systems admit contraction and cut admissibility, and allow a systematic proof-search procedure of formal derivations.

We prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, φ, built up from propositional variables (p,q,r,...) and falsity $(\perp)$ using conjunction $(\wedge)$ , disjunction (∨) and implication (→). Write $\vdash\phi$ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula φ there exists a formula Apφ (effectively computable from φ), containing only variables not equal to p which occur in φ, and such that for (...) all formulas ψ not involving $p, \vdash \psi \rightarrow A_p\phi$ if and only if $\vdash \psi \rightarrow \phi$ . Consequently quantification over propositional variables can be modelled in IpC, and there is an interpretation of the second order propositional calculus, IpC2, in IpC which restricts to the identity on first order propositions. An immediate corollary is the strengthening of the usual interpolation theorem for IpC to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of IpC, the theory of Heyting algebras. In particular we show that a model of IpC2 can be constructed whose algebra of truth-values is equal to any given Heyting algebra. (shrink)

We discuss the interpolation property on some important families of non classical logics, such as intuitionistic, modal, fuzzy, and linear logics. A special paragraph is devoted to a generalization of the interpolation property, uniform interpolation.

We propose a new perspective on logics of computation by combining instantial neighborhood logic INL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {INL}$$\end{document} with bisimulation safe operations adapted from PDL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {PDL}$$\end{document}. INL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {INL}$$\end{document} is a recent modal logic, based on an extended neighborhood semantics which permits quantification over individual neighborhoods plus their contents. This system has a natural interpretation as a (...) logic of computation in open systems. Motivated by this interpretation, we show that a number of familiar program constructors can be adapted to instantial neighborhood semantics to preserve invariance for instantial neighborhood bisimulations, the appropriate bisimulation concept for INL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {INL}$$\end{document}. We also prove that our extended logic IPDL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {IPDL}$$\end{document} is a conservative extension of dual-free game logic, and its semantics generalizes the monotone neighborhood semantics of game logic. Finally, we provide a sound and complete system of axioms for IPDL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {IPDL}$$\end{document}, and establish its finite model property and decidability. (shrink)