Spatial logic
Go to home page
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.
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
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).
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:
- the modal mu-calculus with the closure operator ♢
- ♢ and the tangled closure operators < t >
- ♢, ∀
- ♢, ∀, < t >
- the derivative operator < d >
- < d > and the associated tangled closure operators < dt >
- < d >, ∀
- < 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.
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.
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.
Robert Goldblatt and Ian Hodkinson
Review of Symbolic Logic 13 (2020) 611-632. Copyright Association for Symbolic Logic.
DOI: https://doi.org/10.1017/S1755020319000534
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.