Finitary Inductively Presented Logics*
Solomon Feferman · 1994
Abstract A notion of finitary inductively presented (f.i.p.) logic is proposed here, which includes all syntactically described logics (formal systems) met in practice. A f.i.p. theory FS0 is set up which is universal for all f.i.p. logics; though formulated as a theory of functions and classes of expressions, FS0 is a conservative extension of PRA. The aims of this work are (i) conceptual, (ii) pedagogical and (iii) practical. The system FSo serves under (i) and (ii) as a theoretical framework for the formalization of metamathematics. The general approach may be used under (iii) for the computer implementation of logics. In all cases, the work aims to make the details manageable in a natural and direct way.