Bridges between classical and constructive reasoning for infinitary logic
A survey will be presented on the bridges between classical and constructive reasoning in infinitary logic. At the level of probability we show how the method of conversion of axioms into rules gives a natural approach to Glivenko sequent classes for geometric theories [1, 2]. At the structural level, we show that enriching the syntax of sequents with labels for neighbourhood semantics gives an intuitionistic calculus that shares all the properties of its classical counterpart [3] and that allows to extend to the infinitary setting the modal interpretation of intuitionistic logic [4].
References
[1] Fellin, G, Negri, S. and Orlandelli, E. Glivenko classes and constructive cut elimination in infinitary logic, ms., 2021
[2] Negri, S. Geometric rules in infinitary logic. In O. Arieli and A. Zamansky (eds) Arnon Avron on Semantics and Proof Theory of Non-Classical Logics, Outstanding Contributions to Logic, Springer, pp. 265–293, 2021.
[3] Tesi, M., Negri, S. Neighbourhood semantics and labelled calculus for intuitionistic infinitary logic. Journal of Logic and Computation, 2021, exab040, https://doi.org/10.1093/logcom/exab040.
[4] Tesi, M., Negri, S. Infinitary modal logic and the G ̈odel-McKinsey-Tarski embedding, submitted.
The talk will be held on Zoom. Contact Laura.Crosilla @ ifikk.uio.no for a Zoom-invite.