Towards a Logic for Pragmatics. Assertions and Conjectures
Gianluigi Bellin · Journal of Logic and Computation · 2004
The logic for pragmatics extends classical logic in order to characterize the logical properties of the operators of illocutionary force such as that of assertion and obligation and of the pragmatic connectives which are given an intuitionistic interpretation. Here we consider the cases of assertions and conjectures: the assertion that a mathematical proposition α is true is justified by the capacity to present an actual proof of α, while the conjecture that α is true is justified by the absence of a refutation of α. We give sequent calculi of type G3i and G3im inspired by Girard's LU, with subsystems characterizing intuitionistic reasoning and some forms of classical reasoning with such operators. Extending Gödel, McKinsey, Tarski and Kripke's translations of intuitionistic logic into S4, we show that our sequent calculi are sound and complete with respect to Kripke's semantics for S4.