Translations: generalizing relative expressiveness between logics

TL;DR

This paper develops a broad, formal framework for comparing the expressiveness of different logics, extending beyond model-theoretic approaches to include proof-theoretic and Tarskian logics, and introduces criteria for evaluating translational expressiveness.

Contribution

It proposes a new, general formal criterion for translational expressiveness that overcomes limitations of previous model-theoretic and broader frameworks.

Findings

Analyzes limitations of existing expressiveness criteria.

Introduces a formal criterion for translational expressiveness.

Provides adequacy criteria for comparing logics.

Abstract

There is a strong demand for precise means for the comparison of logics in terms of expressiveness both from theoretical and from application areas. The aim of this paper is to propose a sufficiently general and reasonable formal criterion for expressiveness, so as to apply not only to model-theoretic logics, but also to Tarskian and proof-theoretic logics. For model-theoretic logics there is a standard framework of relative expressiveness, based on the capacity of characterizing structures, and a straightforward formal criterion issuing from it. The problem is that it only allows the comparison of those logics defined within the same class of models. The urge for a broader framework of expressiveness is not new. Nevertheless, the enterprise is complex and a reasonable model-theoretic formal criterion is still wanting. Recently there appeared two criteria in this wider framework, one from Garc\'ia-Matos & V\"a\"an\"anen and other from L. Kuijer. We argue that they are not adequate. Their limitations are analyzed and we propose to move to an even broader framework lacking model-theoretic notions, which we call "translational expressiveness". There is already a criterion in this later framework by Mossakowski et al., however it turned out to be too lax. We propose some adequacy criteria for expressiveness and a formal criterion of translational expressiveness complying with them is given.