university of tampere:
sis/luo-coms:
research:
cis - the tampere research center for information and systems:
research groups:
logic group:
research:

The study of modal logic at University of Tampere concentrates on (finite) model theoretic issues, with the emphasis on questions related to definability theory.

Extensions of modal logic have applications in various fields from economics to artificial intelligence. Studying the expressive power of these extensions serves two purposes. Firstly, it is relevant to applications of modal logic. Secondly, extensions of modal logic often correspond to natural fragments of predicate logic. Therefore, the study of the expressive power of extensions of modal logic is also a study of the expressive power of predicate logic.

Questions related to the expressive power of second-order logic and its fragments, such as Sigma-1-1 and MSO, play a central role in finite model theory. Due to the high expressive power of these languages, problems related to undefinability issues tend to be demanding. By limiting attention to subfragments where the first-order part has been replaced by standard translations of modal formulae, it is often easier to gain insight to the role different logical constructs (such as connectives and quantifiers) play in making the expressive power second-order logic.

Formulae of second-order propositional modal logic consist of a prefix of propositional quantifiers followed by a modal formula. A natural question is whether the expressive power of this logic grows without bound as the number of alternating blocks of universal and existential quantifiers increases. In other words, is the alternation hierarchy of the logic infinite?

**Theorem** ([1]). The alternation hierarchy of second-order
propositional modal logic is infinite.

The theorem solves an open problem of van Benthem from 1983. For more results related to fragments of second-order logic and modal logic, see [2].

[1] Antti Kuusisto,
*A modal perspective on monadic second-order alternation hierarchies*,
Advances in Modal Logic 2008.

[2] Lauri Hella and Antti Kuusisto,
*Monadic Sigma-1-1 and Modal Logic with Quantified Binary Relations*,
Methods for Modalities 2009.

In conventional modal logics, the structures considered are pointed models over a relational vocabulary. A pointed model is a pair (M,w), where M is a model and w is an element in M. A formula is true in (M,w) if it is true at w. Modal logics that are evaluated on pointed models are called 1-dimensional. In n-dimensional modal logic formulas are evaluated at n-tuples (w_1,…,w_n). Tuple (M,w_1,…,w_n) is a n-dimensional model. So, where as in the 1-dimensional case formulas define sets, in the n-dimensional case formulas define n-ary relations. Most common modal logics are 1-dimensional, although in temporal logic the 2-dimensional case is well studied.

Expressive power is a natural measure by which to compare different logics. Although n-dimensional modal logics appear more complex than k-dimensional ones when n>k, it is not clear whether higher dimensional logics have more expressive power.

1) Is it the case that for all k there is an n>k such that there is an n-dimensional modal logic that isn’t expressively equivalent to any k-dimensional modal logic?

2) Is it the case that for every k there is a k-dimensional modal logic that isn’t expressively equivalent to any (k-1)-dimensional modal logic?

If the answer to the first question is “yes” then the dimension hierarchy is infinite, and if the answer to the second question is “yes” then the hierarchy is strict. We conjecture that the answer to both questions is affirmative.

Danièle Beauquier and Alexander Rabinovich proved in the article “Monadic Logic of Order over Naturals has no Finite Base” that there is no 1-dimensional modal logic with finitely many modalities that is expressively equivalent to monadic second-order logic over word models. Lauri Hella and Tero Tulenheimo have constructed a 2-dimensional modal logic with finitely many modalities that is expressively equivalent to monadic second-order logic over word models, thus proving that there is a 2-dimensional modal logic with finitely many modalities that isn’t expressively equivalent to any 1-dimensional modal logic with finitely many modalities.

It is well-known that Kripke semantics is not general enough as a basis for all systems of modal logic. Scott-Montague semantics is a natural generalization of Kripke semantics that solves such problems. Instead of a binary relation, in a Scott-Montague model M the interpretation of the modal operator ◻ is given by a set function F: P(W)→P(W). The truth condition for a formula ◻ϕ is: M,w⊨◻ϕ if and only if w is in the truth set {v∈W | M,v⊨ϕ} of the formula ϕ.

In the case the set of states W of the model M is finite, the set function F can be thought as a vector valued Boolean function f: {0,1}^n→{0,1}^n: just enumerate the elements of W as a_1,...,a_n, and let f(b_1,...,b_n) = (c_1,...,c_n), where c_i=1 if and only if a_i∈F({a_j | c_j=1}). Conversely, every Boolean function f: {0,1}^n→{0,1}^n gives rise to a corresponding set function F: P(W)→P(W). Thus, it is natural to look for connections between definability of classes of Scott-Montague frames and axiomatizations of classes of Boolean functions; this idea was the starting point of the article [CoHeKi08].

The most natural classes of Boolean functions to consider are the so-called *clones*.
A class is a clone, if it contains all projections and is closed under composition of functions.
It is known that every clone can be axiomatized by a finite set of *functional terms*.
Using the correspondence explained above, we found in [CoHeKi08] a translation of functional
terms into *uniform degree-1* formulas of modal logic, which axiomatizes the corresponding class of
Scott-Montague frames. In particular, we characterized the class of those Kripke frames in terms of the
clone Λ_1 generated by the constant 1 and conjunction. Furthermore, we characterized classes of
Kripke style frames with modified (exlusive or based) semantics in terms of the clones L, L_0 and LS
of linear Boolean functions.

**THE UNIVERSITY**

Research

Admissions

Studies

News

Cooperation and Services

About Us

**CURRENT ISSUES**

Research & Study

Tampere3

Vacancies