Spatial logic

Go to home page

The modal logic of affine planes is not finitely axiomatisable

Ian Hodkinson and Altaf Hussain
J. Symbolic Logic 73 (2008) 940-952.
We consider a modal language for affine planes, with two sorts of formulas (for points and lines) and three modal diamonds. To evaluate formulas, we regard an affine plane as a Kripke frame with two sorts (points and lines) and three modal accessibility relations, namely the point-line and line-point incidence relations and the parallelism relation between lines. We show that the modal logic of affine planes in this language is not finitely axiomatisable.

Simple completeness proofs for some spatial logics of the real line

Ian Hodkinson
in: Proc. 12th Asian Logic Conference, R. Downey, J. Brendle, R. Goldblatt, B. Kim (eds), World Scientific, 2013, pp. 155-177.
McKinsey-Tarski (1944), Shehtman (1999), and Lucero-Bryan (2011) proved completeness theorems for modal logics with modalities ☐, ☐ and ∀, and [d] and ∀, respectively, with topological semantics over the real numbers. We give short proofs of these results using lexicographic sums of linear orders.

The finite model property for logics with the tangle modality

Robert Goldblatt and Ian Hodkinson
Studia Logica 106 (2018) 131-166.
The tangle modality is a propositional connective that extends basic modal logic to a language that is expressively equivalent over certain classes of finite frames to the bisimulation-invariant fragments of both first-order and monadic second-order logic. This paper axiomatises several logics with tangle, including some that have the universal modality, and shows that they have the finite model property for Kripke frame semantics. The logics are specified by a variety of conditions on their validating frames, including local and global connectedness properties. Some of the results have been used to obtain completeness theorems for interpretations of tangled modal logics in topological spaces (in the paper below).

Spatial logic of tangled closure operators and modal mu-calculus

Robert Goldblatt and Ian Hodkinson
Annals of Pure and Applied Logic 168 (2017) 1032-1090
DOI 10.1016/j.apal.2016.11.006
There has been renewed interest in recent years in McKinsey and Tarski's interpretation of modal logic in topological spaces and their proof that S4 is the logic of any separable dense-in-itself metric space.  Here we extend this work to the modal mu-calculus and to a logic of tangled closure operators that was developed by Fernandez-Duque after these two languages had been shown by Dawar and Otto to have the same expressive power over finite transitive Kripke models. We prove that this equivalence remains true over topological spaces.  We extend the McKinsey-Tarski topological 'dissection lemma'.  We also take advantage of the fact (proved in the preceding paper) that various tangled closure logics with and without the universal modality ∀ have the finite model property in Kripke semantics. These results are used to construct a representation map (also called a d-p-morphism) from any dense-in-itself metric space X onto any finite connected locally connected serial transitive Kripke frame.
This yields completeness theorems over X for a number of languages:
  1. the modal mu-calculus with the closure operator ♢
  2. ♢ and the tangled closure operators < t >
  3. ♢, ∀
  4. ♢, ∀, < t >
  5. the derivative operator < d >
  6. < d > and the associated tangled closure operators < dt >
  7. < d >, ∀
  8. < d >, ∀, < dt >
Soundness also holds, if: (a) for languages with ∀, X is connected; (b) for languages with < d >, X validates the well known axiom G1.  For countable languages without ∀, we prove strong completeness.  We also show that in the presence of ∀, strong completeness fails if X is compact and locally connected.

The Tangled Derivative Logic of the Real Line and Zero-Dimensional Spaces

Robert Goldblatt and Ian Hodkinson
Proc. Advances in Modal Logic (AiML-16), vol. 11, College Publications, 2016, 342-361.
In a topological setting in which the diamond modality is interpreted as the derivative (set of limit points) operator, we study a 'tangled derivative' connective that assigns to any finite set of propositions the largest set in which all those propositions are strictly dense. Building on earlier work of ourselves and others, we axiomatise the resulting logic of the real line. We then show that the logic of any zero-dimensional dense-in-itself metric space is the 'tangled' extension of KD4, eliminating an assumption of separability in previous results for zero-dimensional spaces. This requires new kinds of 'dissection lemma' in the sense of McKinsey-Tarski. We extend the analysis to include the universal modality, and also show that the tangled extension of KD4 has a strong completeness result for topological models that fails for its Kripke semantics.

Tangled closure algebras

Robert Goldblatt and Ian Hodkinson
Categories and General Algebraic Structures with Applications 7 (2017) 9-31.
The tangled closure of a collection of subsets of a topological space is the largest subset in which each member of the collection is dense. This operation models a logical 'tangle modality' connective, of significance in finite model theory. Here we study an abstract equational algebraic formulation of the operation which generalises the McKinsey-Tarski theory of closure algebras. We show that any dissectable tangled closure algebra, such as the algebra of subsets of any metric space without isolated points, contains copies of every finite tangled closure algebra. We then exhibit an example of a tangled closure algebra that cannot be embedded into any complete tangled closure algebra, so it has no MacNeille completion and no spatial representation.

Strong completeness of modal logics over 0-dimensional metric spaces

Robert Goldblatt and Ian Hodkinson
Review of Symbolic Logic 13 (2020) 611-632. Copyright Association for Symbolic Logic.
We prove strong completeness results for some modal logics with the universal modality, with respect to their topological semantics over 0-dimensional dense-in-themselves metric spaces. We also use failure of compactness to show that, for some languages and spaces, no standard modal deductive system is strongly complete.