Decision procedures for logics of consequential implication.
Claudio Pizzi · Notre Dame Journal of Formal Logic · 1991
The paper introduces a new kind of implication named "consequential implication", which is a variant of traditional connexive implication lacking a certain monotonicity property and allowing the distinction between analytic and synthetic conditionals.A system CI.O for analytical consequential implication is proved to be definitionally equivalent to Feys-von Wright system T, and so decidable by the standard tableaux method.Three systems, named CI*0, CI*1, and CI*2, are then introduced as axiomatic and linguistic extensions of CI.O in which synthetic conditionals are definable.It is shown that these three systems may be translated into certain extensions of T whose language contains new linguistic objects named "quasi-variables".Since the latter systems are proved to be decidable by the tableaux method, it follows that this method gives a decision procedure also for the related systems of consequential implication.Points (a) and (b) are strictly interlinked: if we had (p A q) CI q, then we would have both (p A ~yp) CI p and (p A -ι/?) CI -ι/?, which would be a coun-