Sara Negri

In a recent paper, Negri and Pavlović (Studia Logica 1–35, 2020) have formulated a decidable sequent calculus for the logic of agency, specifically for a deliberative see-to-it-that modality, or dstit. In that paper the adequacy of the system is demonstrated by showing the derivability of the axiomatization of dstit from Belnap et al. (Facing the future: agents and choices in our indeterminist world. Oxford University Press, Oxford, 2001). And while the influence of the latter book on the study of logics of agency cannot be overstated, we note that this is not the only axiomatization of that modality available. In fact, an earlier (and arguably purer) one was offered in Xu (J Philosophical Logic 27(5):505–552, 1998). In this article we fill this lacuna by proving that this alternative axiomatization is likewise readily derivable in the system of Negri and Pavlović (Studia Logica 1–35, 2020).

A constructivisation of the cut-elimination proof for sequent calculi for classical, intuitionistic and minimal infinitary logics with geometric rules—given in earlier work by the second author—is presented. This is achieved through a procedure where the non-constructive transfinite induction on the commutative sum of ordinals is replaced by two instances of Brouwer’s Bar Induction. The proof of admissibility of the structural rules is made ordinal-free by introducing a new well-founded relation based on a notion of embeddability of derivations. Additionally, conservativity for classical over intuitionistic/minimal logic for the seven (finitary) Glivenko sequent classes is here shown to hold also for the corresponding infinitary classes.

The contraction-free sequent calculus G4 for intuitionistic logic is extended by rules following a general rule-scheme for nonlogical axioms. Admissibility of structural rules for these extensions is proved in a direct way by induction on derivations. This method permits the representation of various applied logics as complete, contraction- and cut-free sequent calculus systems with some restrictions on the nature of the derivations. As specific examples, intuitionistic theories of apartness and order are treated.

A sequent calculus is given in which the management of weakening and contraction is organized as in natural deduction. The latter has no explicit weakening or contraction, but vacuous and multiple discharges in rules that discharge assumptions. A comparison to natural deduction is given through translation of derivations between the two systems. It is proved that if a cut formula is never principal in a derivation leading to the right premiss of cut, it is a subformula of the conclusion. Therefore it is sufficient to eliminate those cuts that correspond to detour and permutation conversions in natural deduction.

Large portions of mathematics such as algebra and geometry can be formalized using first-order axiomatizations. In many cases it is even possible to use a very well-behaved class of first-order axioms, namely, what are called coherent or geometric implications. Such class of axioms can be translated to inference rules that can be added to a sequent calculus while preserving its structural properties. In this work, this fundamental result is extended to their infinitary generalizations as extensions of sequent calculi for both classical and intuitionistic infinitary logic. As an application, a simple proof of the infinitary Barr’s theorem without the axioms of choice is shown.