The strong decidability of cut logics. II. Generalizations.
E. William Chapin · Notre Dame Journal of Formal Logic · 1971
In the first part of this paper [1] we discussed the result of restricting the number of applications of the rule modus ponens in a certain class of partial propositional calculi.Here we shall generalize the results of that paper to partial propositional calculi in general, and to the cut versions of modal logics.We first recall some definitions.For details, the reader is referred to [1].By a partial propositional calculus, we shall mean a triple (M,R,N) where M is a finite set of well-formed formulae which are theorems of the classical propositional calculus, R is either the rule modus ponens (MP) or the rule MP together with the rule simultaneous substitution (SS), or the rule MP together with the rule substitution (S), and N is a non-negative integer or infinity.If N is infinity, the calculus is to be thought of as the usual calculus with the rules R and the axioms M. The calculi with N finite are the same calculi with the restriction that the rule MP may be applied N times or fewer only.The calculi with N finite will be called cut-calculi.(This definition will be generalized for the case of modal logics.)Any calculus of either of the above type^?is called decidable if there exists an effective method, given any well-formed formula of the calculus, for deciding whether that formula is a theorem of the given calculus.Such a calculus will be called strongly decidable if one can effectively find a finite set of well-formed formulae such that the set of theorems of the calculus coincides with the set of SS instances of the given set of formulae.2. Partial propositional calculi.In the first part of this paper, we restricted ourselves to calculi where implication (D) and a constant false (f) were the only connectives present.Here we place no restriction on what (finite number of) connectives and constants may be present but we do assume that 3 is present, since we wish to have MP as one of our rules.(If this is not the case, the results still hold, but are not of as great interest.)We say that a singulary connective is of degree one, a binary connective is of degree two, etc., thus associating a finite integer with each connective.Since we are placing no restrictions on the number of times that the rule S