Proof systems for Geometric theories (PROGEO)
Resumo
We plan to study the problem of finding conservative extensions of first order logics. In this project we intend to establish a systematic procedure for adding geometric theories in both intuitionistic and classical logics, as well as to extend this procedure to bipolar axioms, a generalization of the set of geometric axioms. This way, we obtain proof systems for several mathematical theories, such as lattices, algebra and projective geometry, being able to reason about such theories using automated deduction.
Referências
Danos, V., Joinet, J.-B., and Schellinx, H. (1995). LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In Girard, J.-Y., Lafont, Y., and Regnier, L., editors, Advances in Linear Logic, number 222 in London Mathematical Society Lecture Note Series, pages 211–224. Cambridge University Press.
Dyckhoff, R. and Negri, S. (2015). Geometrisation of first-order logic. The Bulletin of Symbolic Logic, 21(2):123–163.
Gentzen, G. (1935a). Investigations into logical deduction. In Szabo, M. E., editor, The Collected Papers of Gerhard Gentzen, pages 68–131. North-Holland, Amsterdam.
Gentzen, G. (1935b). Untersuchungen über das logische schliessen. Mathematische Zeitschrift, 39:176–210.
Liang, C. and Miller, D. (2007). Focusing and polarization in intuitionistic logic. In Duparc, J. and Henzinger, T. A., editors, CSL 2007: Computer Science Logic, volume 4646 of LNCS, pages 451–465. Springer.
Liang, C. and Miller, D. (2009). Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci., 410(46):4747–4768.
Marin, S., Miller, D., Pimentel, E., and Volpe, M. (2020). From axioms to synthetic inference rules via focusing. Available at https://drive.google.com/file/d/ 1_gNtKjvmxyH7T7VwpUD0QZtXARei8t5K/view.
Negri, S. (2003). Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem. Arch. Math. Log., 42(4):389–401.
Negri, S. (2005). Proof analysis in modal logic. J. Philosophical Logic, 34(5-6):507– 544.
Negri, S. (2016). Proof analysis beyond geometric theories: from rule systems to systems of rules. J. Log. Comput., 26(2):513–537.
Negri, S. and von Plato, J. (1998). Cut elimination in the presence of axioms. Bulletin of Symbolic Logic, 4(4):418–435.
Negri, S. and von Plato, J. (2011). Proof Analysis - a contribution to Hilbert’s last problem. Cambridge University Press.
Simpson, A. K. (1994). The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, College of Science and Engineering, School of Informatics, University of Edinburgh.
Viganò, L. (2000). Labelled Non-Classical Logics. Kluwer Academic Publishers.