2017/06/26 by Diego Pinheiro Fernandes, Fernandes, Diego Pinheiro
Computer Science · #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Advanced Algebra and Logic
paper · pdf · doi:10.48550/arxiv.1706.08481
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ía-Matos & Väänänen 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.