Axiomatisation, canonicity
Go to home page
| Canonicity (in algebraic logic)
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].
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.
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.
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.
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.
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.
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.
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, 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.
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.
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.
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.
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.
14.
Canonicity in power and modal logics of finite achronal width
We develop a method for showing that various modal logics that are valid in their countably generated canonical Kripke frames must also be valid in their uncountably generated ones. This is applied to many systems, including the logics of finite width, and a broader class of multimodal logics of `finite achronal width' that are introduced here.