Sara Negri

November 6, 2015
  1. July 2016
From neighbourhood semantics to analytic proof systems for non-normal modal logics

Labelled sequent calculi provide, through an internalization of possible worlds’ semantics, a versatile formalism for the proof theory of large families of philosophical logics  (Negri 2005). Recently, the method has been extended to cover any modal logic characterized by first-order frame conditions  (Dyckhoff and Negri 2015). The semantics of important intensional connectives, such as the counterfactual conditional or the modalities of non-normal systems, however, escapes such analysis and requires the more general neighbourhood semantics.

In the first part of the talk we’ll show how the formalism of labelled calculi can be extended to encompass neighbourhood semantics so as to obtain calculi with invertible rules and admissible structural rules (Negri 2016). In the second part, we shall present for the logic of conditional beliefs the development of a calculus that starts from a conversion of plausibility models to neighbourhood models (Girlando, Negri, Olivetti, Risch 2016).

References

  • Dyckhoff, R. and S. Negri (2015) Geometrization of first-order logic, The Bulletin of Symbolic Logic, vol. 21, pp. 123-163.
  • Negri, S.  (2005) Proof analysis in modal logic. Journal of Philosophical Logic, vol. 34, pp. 507-544.
  • Negri, S. (2016) Proof theory for non-normal modal logics: The neighbourhood  formalism and basic results, IfCoLog JJournal of Logic and its Applications, to appear.
  • Girlando, M., S. Negri, N. Olivetti, V. Risch (2016) The logic of conditional beliefs: neighbourhood semantics and sequent calculus, AiML’16, to appear.
  1. October 2015
Glivenko sequent classes in the light of structural proof theory

In 1968, Orevkov presented proofs of conservativity of classical over intuitionistic and minimal predicate logic with equality for seven classes of sequents, what are known as Glivenko classes. The proofs of these results, important in the literature on the constructive content of classical theories, have remained somehow cryptic. In this talk, examples and direct proofs for more general extensions are given for each class by exploiting the structural properties of G3 sequent calculi; for five of the seven classes the results are strengthened to height-preserving, statements, and it is further shown that the constructive and minimal proofs are identical in structure to the classical proof from which they are obtained.