Metacompleteness.
Robert K. Meyer · Notre Dame Journal of Formal Logic · 1976
In [1], a logic was called coherent provided that it could plausibly be interpreted in its own metalogic.By deepening and making more intuitive the logical analysis implicit in [l], we develop here a kindred notion of metacompleteness; & logic is metacomplete provided that exactly the sentences true on a certain preferred interpretation of that logic in its metalogic are theorems.Acquaintance with [l] is not presupposed.We shall show in particular that a number of familiar logics, e.g., of the intuitionist, modal, and relevant families, are metacomplete, and that accordingly these logics share with intuitionist calculi two interesting properties:is a theorem, so is some substitution instance A{t), for some term t.