To page body
university of tampere: sis/luo-coms: research: cis - the tampere research center for information and systems: research groups: logic group: research:
Faculties of Natural and Communication SciencesUniversity of TampereFaculties of Natural and Communication Sciences
CIS - The Tampere Research Center for Information and Systems

Modal logic at UTA

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

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.

Multidimensional Modal Logic

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.

Scott-Montague semantics and Boolean functions

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.

Maintained by:
Last update: 24.12.2011 22.59 Muokkaa

University of Tampere
+358 3 355 111

FINEEC Audited HR Excellence in Research

Cooperation and Services
About Us

Research & Study

Career Services
Finnish Social Science Data Archive
Centre for International Education
IT services
Language Centre
Language Services
Registrar's Office
Sports Activities
» more

Teaching schedules
Curricula guides
Student's Desktop

Andor search
Renew your loans
UTA intranet
Office 365 webmail
Uta webmail
Electronic exam service
Examination results