Axiomatisation, canonicity

Go to home page

1. An axiomatisation of Until and Since over the real numbers

D M Gabbay and I M Hodkinson
Journal of Logic and Computation 1 (1990) 229-260.
We give a Hilbert style axiomatisation of the temporal logic with connectives Until and Since for the real numbers, using an irreflexivity rule. We prove independence of the axioms, and completeness for this semantics with respect to single formulas.

A better proof is in the book here.

The use of the irreflexivity rule was later eliminated by Reynolds [An axiomatization for Until and Since over the Reals without the IRR rule, Studia Logica 51 (1992) 165-194].

2. All normal extensions of S5-squared are finitely axiomatizable

N Bezhanishvili and I Hodkinson
Studia Logica 78 (2004) 443-457.  ILLC preprint PP-2003-25
We prove that every normal extension of the bi-modal system S5 x S5 is finitely axiomatizable and that every proper normal extension has NP-complete satisfiability problem.

3. Erdös graphs resolve Fine's canonicity problem

Robert Goldblatt, Ian Hodkinson, and Yde Venema
Bull. Symbolic Logic 10 no. 2 (June 2004), 186-208.  ILLC preprint PP-2003-26
We show that there exist continuum-many equational classes of Boolean algebras with operators that are not generated by the complex algebras of any first-order definable class of relational structures. Using a variant of this construction, we resolve a long-standing question of Fine, by exhibiting a bimodal logic that is valid in its canonical frames, but is not sound and complete for any first-order definable class of Kripke frames (a monomodal example can then be obtained using simulation results of Thomason).  The constructions use the result of Erdös that there are finite graphs with arbitrarily large chromatic number and girth.

4. On canonical modal logics that are not elementarily determined

Robert Goldblatt, Ian Hodkinson, and Yde Venema
Logique et Analyse 181 (2003) 77-101.
There exist modal logics that are validated by their canonical frames but are not sound and complete for any elementary class of frames. Continuum many such bimodal logics are exhibited, including one of each degree of unsolvability, and all with the finite model property. Monomodal examples are also constructed that extend K4 and are related to the proof of non-canonicity of the McKinsey axiom.

We dedicate this paper to Max Cresswell, a pioneer in the study of canonicity, on the occasion of his 65th birthday.

5. Canonical varieties with no canonical axiomatisation

Ian Hodkinson and Yde Venema
Trans. Amer. Math. Soc. 357 (2005), 4579-4605.
This paper is written in algebraic terms, but is relevant to modal logic.  We give a simple example of a variety V of modal algebras that is canonical but cannot be axiomatised by canonical equations or first-order sentences.  This can be viewed modally as a canonical modal logic that cannot be axiomatised by canonical formulas.  We then show that the variety RRA of representable relation algebras, although canonical, has no canonical axiomatisation.  Indeed, we show that every axiomatisation of these varieties involves infinitely many non-canonical sentences.

Using probabilistic methods of Erdös, we construct an infinite sequence G0, G1, ... of finite graphs with arbitrarily large chromatic number, such that each Gn is a bounded morphic image of Gn+1 and has no odd cycles of length at most n. The inverse limit of the sequence is a graph with no odd cycles and hence is 2-colourable. It follows that a modal algebra (respectively, a relation algebra) obtained from the Gn satisfies arbitrarily many axioms from a certain axiomatisation of V (RRA), while its canonical extension satisfies only a bounded number of them. It now follows by compactness that V (RRA) has no canonical axiomatisation. A variant of this argument shows that there is no axiomatisation using finitely many non-canonical sentences.

6. Hybrid formulas and elementarily generated modal logics

Ian Hodkinson
Notre Dame J. Formal Logic 47 (2006) 443-478.
We show that the modal logics of elementary classes of Kripke frames are precisely those logics that can be captured by sets of pure positive hybrid sentences with arbitrary existential and relativised universal quantification over nominals.  Each such hybrid sentence generates an infinite set of modal formulas called 'approximants', which together axiomatise a canonical modal logic that is sound and complete for the class of frames validating the hybrid sentence.  This generalises to sets of hybrid sentences.  The proof is analogous to standard proofs of Sahlqvist's theorem.

7. The McKinsey-Lemmon logic is barely canonical

Robert Goldblatt and Ian Hodkinson
Australasian J. Logic 5 (2007) 1-19.
We study a canonical modal logic introduced by Lemmon, and axiomatised by an infinite sequence of axioms generalising McKinsey's formula.  We prove that the class of all frames for this logic is not closed under elementary equivalence, and so is non-elementary.  We also show that any axiomatisation of the logic involves infinitely many non-canonical formulas.

8. 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.

9. Non-finite axiomatizability and undecidability of interval temporal logics with C, D, and T

Ian Hodkinson, Angelo Montanari, and Guido Sciavicco
In: Computer Science Logic (Proc. CSL 2008), M. Kaminski and S. Martini (Eds.), LNCS 5213, 2008, pp. 308-322.
Interval logics are an important area of computer science.  Although attention has been mainly focused on unary operators, an early work by Venema (1991) introduced an expressively complete interval logic language called CDT, based on binary operators, which has many potential applications and a strong theoretical interest.  Many very natural questions about CDT and its fragments, such as (non-)finite axiomatizability and (un-)decidability, are still open (as a matter of fact, only a few undecidability results, including the undecidability of CDT, are known).  In this paper, we answer most of these questions, showing that almost all fragments of CDT, containing at least one binary operator, are neither finitely axiomatizable with standard rules nor decidable.  A few cases remain open.

10. Axiomatizing hybrid logic using modal logic

Ian Hodkinson and Louis Paternault
Journal of Applied Logic 8 (2010) 386-396, doi:10.1016/j.jal.2010.08.005.
We study hybrid logics with nominals and 'actuality' operators @.  We recall the method of ten Cate, Marx, and Viana to simulate hybrid logic using modalities and 'nice' frames, and we show that the hybrid logic of a class of frames is the modal logic of the class of its corresponding nice frames.  Using these results, we show how to axiomatize the hybrid logic of any elementary class of frames.  Then we study quasimodal logics, which are hybrid logics axiomatized by modal axioms together with basic hybrid axioms common to any hybrid logic, using only orthodox inference rules.  We show that the hybrid logic of any elementary modally definable class of frames, or of any elementary class of frames closed under disjoint unions, bounded morphic images, ultraproducts and generated subframes, is quasimodal.  We also show that the hybrid analogues of modal logics studied by McKinsey--Lemmon and Hughes are quasimodal.

11. Sahlqvist theorem for modal fixed point logic

Nick Bezhanishvili and Ian Hodkinson
Theoretical Computer Science 424 (2012) 1-19.
We define Sahlqvist fixed point formulas. By extending the technique of Sambin and Vaccaro we show that (1) for each Sahlqvist fixed point formula $\varphi$ there exists an LFP-formula $\chi(\varphi)$, with no free first-order variable or predicate symbol, such that a descriptive $\mu$-frame (an order-topological structure that admits topological interpretations of least fixed point operators as intersections of clopen pre-fixed points) validates $\varphi$ iff $\chi(\varphi)$ is true in this structure, and (2) every modal fixed point logic axiomatized by a set $\Phi$ of Sahlqvist fixed point formulas is sound and complete with respect to the class of descriptive $\mu$-frames satisfying $\{\chi(\varphi): \varphi\in \Phi\}$. We also give some concrete examples of Sahlqvist fixed point logics and classes of descriptive $\mu$-frames for which these logics are sound and complete.

12. Simple completeness proofs for some spatial logics of the real line

Ian Hodkinson
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 [A], and [d] and [A], respectively, with topological semantics over the real numbers.  We give short proofs of these results using lexicographic sums of linear orders.

13. On the Priorean temporal logic with 'around now' over the real line

Ian Hodkinson
J. Logic and Computation 24 (2014) 1071-1110. doi: 10.1093/logcom/ext056
Open access article
We consider the temporal language with the Priorean operators G and H expressing that a formula is true at all future times and all past times, plus a box operator expressing that a formula is true throughout some open interval containing the evaluation time (i.e., it is true 'around now'). We show that the logic of real numbers time in this language is finitely axiomatisable, answering an implicit question of Shehtman (1993). We also show that the logic has PSPACE-complete complexity, but is not Kripke complete and has no strongly complete axiomatisation.