Foundations for the formalization of metamathematics and axiomatizations of consequence theories Original Research Article

This paper deals with Tarskiʹs first axiomatic presentations of the syntax of deductive system. Andrzej Grzegorczykʹs significant results which laid the foundations for the formalization of metalogic, are touched upon briefly. The results relate to Tarskiʹs theory of concatenation, also called the theory of strings, and to Tarskiʹs ideas on the formalization of metamathematics. There is a short mention of authorʹs research in the field. The main part of the paper surveys research on the theory of deductive systems initiated by Tarski, in particular research on (i) the axiomatization of the general notion of consequence operation, (ii) axiom systems for the theories of classic consequence and for some equivalent theories, and (iii) axiom systems for the theories of nonclassic consequence. In this paper the results of Jerzy Słupeckiʹs research are taken into account, and also the authorʹs and other people belonging to his circle of scientific research. Particular study is made of his dual characterization of deductive systems, both as systems in regard to acceptance (determined by the usual consequence operation) and systems in regard to rejection (determined by the so-called rejection consequence). Comparison is made, therefore, with axiomatizations of the theories of rejection and dual consequence, and the theory of the usual consequence operation.