Involution as a basis for propositional calculi.
Michael B. Smyth · Notre Dame Journal of Formal Logic · 1974
Given two sets of propositions, S x and S 2 , we may say that the relation of involution holds between S 1 and S 2 -or simply that S x involves S 2 -provided that, if all elements of S λ are true, then at least one element of S 2 is true.The notion was introduced by Carnap [3], and treated at length by Kneale [7].According to these authors it may profitably be taken, in place of entailment (of which it is a generalization), as the primary object of study in logic.In developing its properties, they treat it solely as a metalogical relation between sets of propositions in an involution-free system; nested involutions do not occur.It is interesting to enquire what happens if, on the model of existing implicational calculi, involution is treated rather as a primitive operator within a system.This has been done by Duthie [4].His enquiry is, however, somewhat restricted in scope, being concerned almost exclusively with the question of avoiding the (so-called) paradoxes of implication.Apart from this, the nearest approach to an involutional calculus appears to be the 'deduction-logic' of Lorenzen [11] (also Kutschera [9]).This is formulated in terms of a primitive operator ->, on the left of which may appear a variable number of arguments; the consequent, however, is restricted to have exactly one formula.In the present paper an attempt is made to develop a less restricted theory.It is shown that, by varying the inference rules, purely involutional calculi may be constructed that are substantially equivalent to the classical and intuitionistic propositional calculi, and to the modal systems T, S4, S5.Some of the applications are discussed in the final section.1 The formalism and its interpretation.The basic vocabulary shall consist of: i) A denumerable set p oί proposition letters (or atomic formulas).ii) A logical constant, denoted by '->'.iii) Auxiliary symbols: comma, parentheses.Further auxiliary symbols, used for special purposes: the star *, and the 'signs' T, F.The set of formulas is defined inductively by: