Towards a logic for pragmatics. Assertions and conjectures.

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 alpha is true is justified by the capacity to present an actual proof of alpha, while the conjecture that alpha is true is justified by the absence of a refutation of alpha. 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 Goedel, 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.