A syntactical characterization of structural completeness for implicational logics

Abstract

Let P, Q, Q0, Q1,... be propositional formulae in {' — }, i.e. they are formulae built up from the propositional variables p0, p1, . . . by use of the operator ^. The structural consequence operation determined in {' — )• by (the fragment) of intuitionistic logic is denoted by CH and the one determined by intuitionistic logic in {^, A, V, —} is denoted by CI. We examine the problem of structural completeness, with respect to arbitrary finitary and infinitary rules, of any structural consequence operation C in {' — )• such that C > CH. We prove that the structurally complete extension of C is an extension of C with a certain family of schematically defined rules; the same rules are used for each C. The cardinality of the family is continuum and the family cannot be reduced to a countable one. It means that the structurally complete extension of CI is not countably axiomatizable by schematic rules. The paper settles a question raised by Professor Wolfgang Rautenberg in [4] which provided an initial stimulus for the present work (Fragment tekstu).