A pragmatic interpretation of substructural logics

Summary

Abstract Following work by Dalla Pozza and Garola [2, 3] on a pragmatic interpretation of intuitionistic and deontic logics, which has given evidence of their compatibility with classical semantics, we present sequent calculus system ILP formalizing the derivation of assertive judgements and obligations from mixed contexts of assertions and obligations and we prove the cut-elimination theorem for it. For the formalization of real-life normative systems it is essential to consider inferences from mixed contexts of assertions and obligations, and also of assertions justifiable relatively to a given state of information and obligations valid in a given normative system. In order to provide a formalization of the notion of causal implication and its interaction with obligations, the sequents of ILP have two areas in the antecedent, expressing the relevant and the ordinary intuitionistic consequence relation, respectively. To provide a pragmatic interpretation of reasoning with the linear consequence relation we consider the deductive properties of pragmatic schemes where the operators of illocutionary force are unknown (free logic of pragmatic force). We introduce an auxiliary system ILLP which formalizes such a logic, and has substitution rules that allow us to derive the desired mixed sequents. It is shown that in order to permit non-uniform susbtitutions and to preserve Hume's law (the underivability of obligations from truth-asserting judgements only and the potential ineffectuality of norms) ILLP must indeed be based on the linear consequence relation. It is also argued that the above uses of linear and relevant logics are perfectly compatible with a theory of pragmatics in a classical semantical setting and immune from popular confusions about the intuitive interpretations of substructural logics.

Preface Most forms of human reasoning can be formalized and those which deserve such a treatment also benefit from it. Not all philosophers may agree with such a statement, but never mind: the most distinguished opponent of the formalization of mathematical reasoning in the 20th century, Brouwer, was luckily contradicted by his followers and sympathisers, to whom we owe the beautifully insightful constructions of intuitionistic logic, from Heyting's axiomatization and informal semantics of proofs to Gentzen and Prawitz's natural deduction NJ, from Curry and Howard's correspondence between NJ and the typed lambda calculus to categorical logic, and so on and on.