## Abstract

This thesis studies the succinctness of various logics using formula size games. The succinctness of a logic refers to the size of formulas required to express properties. Formula size games are some of the most successful methods of proof for results on succinctness. The contribution of the thesis is twofold. Firstly, we deﬁne formula size games for several logics, providing methods for future research. Secondly, we use these games and other methods to prove results on the succinctness of the studied logics.

More precisely, we develop new parameterized formula size games for basic modal logic, modal μ-calculus, propositional team logic and generalized regular expressions. For the generalized regular expression game we introduce variants that correspond to regular expressions and the newly deﬁned RE over star-free expressions, where stars do not occur inside complements.

We use the games to prove a number of succinctness results. We show that ﬁrst-order logic is non-elementarily more succinct than both basic modal logic and modal μ-calculus. We conduct a systematic study of the succinctness of deﬁning common atoms of dependency in propositional team logic. We reprove a classic non-elementary succinctness gap between ﬁrst-order logic and regular expressions in a much simpler way and establish a hierarchy of expressive power for the number of stars in RE over star-free expressions.

Many of the above results utilize explicit formulas in addition to game arguments. We use such formulas and a type counting argument to obtain non-elementary lower and upper bounds for the succinctness of deﬁning single words in ﬁrst-order logic and monadic second-order logic.

More precisely, we develop new parameterized formula size games for basic modal logic, modal μ-calculus, propositional team logic and generalized regular expressions. For the generalized regular expression game we introduce variants that correspond to regular expressions and the newly deﬁned RE over star-free expressions, where stars do not occur inside complements.

We use the games to prove a number of succinctness results. We show that ﬁrst-order logic is non-elementarily more succinct than both basic modal logic and modal μ-calculus. We conduct a systematic study of the succinctness of deﬁning common atoms of dependency in propositional team logic. We reprove a classic non-elementary succinctness gap between ﬁrst-order logic and regular expressions in a much simpler way and establish a hierarchy of expressive power for the number of stars in RE over star-free expressions.

Many of the above results utilize explicit formulas in addition to game arguments. We use such formulas and a type counting argument to obtain non-elementary lower and upper bounds for the succinctness of deﬁning single words in ﬁrst-order logic and monadic second-order logic.

Original language | English |
---|---|

Place of Publication | Tampere |

ISBN (Electronic) | 978-952-03-2541-1 |

Publication status | Published - 2022 |

Publication type | G5 Doctoral dissertation (articles) |

### Publication series

Name | Tampere University Dissertations - Tampereen yliopiston väitöskirjat |
---|---|

Volume | 659 |

ISSN (Print) | 2489-9860 |

ISSN (Electronic) | 2490-0028 |