De Martin Polo, F. (forthcoming) A note on Cut-elimination for intuitionistic logic with Actuality
Logic Journal of the IGPL
[Preprint]
Abstract. In this paper, we investigate the proof theory of a modal expansion of intuitionistic propositional logic obtained by adding an 'actuality' operator among the connectives. This logic was initially considered by L. Humberstone, and, more recently, also by S. Niki and H. Omori to present a possible application of intuitionism to empirical discourse. Niki and Omori's idea to consider the notion of actuality based on intuitionistic logic was presented, among other things, using Gentzen sequents. Unfortunately, their proof system is not cut-free. In this paper, we define another proof system for Niki and Omori’s logic, namely a hypersequent calculus, and present a proof of cut-elimination for it.
De Martin Polo, F. (2025) Fusion, Fission, and Ackermann’s Truth Constant in Relevant Logics: A Proof-Theoretic Investigation
In: New Directions in Relevant Logic. Ed by Sedlár, I., Standefer, S., Tedder, A. Trends in Logic, vol 63. Springer, Cham
DOI: 10.1007/978-3-031-69940-5_12
[Preprint]
Abstract. The aim of this paper is to provide a proof-theoretic characterization of relevant logics including fusion and fission connectives, as well as Ackermann’s truth constant. We achieve this by employing the well-established methodology of labelled sequent calculi. After having introduced several systems, we will conduct a detailed proof-theoretic analysis, show a Cut-admissibility theorem, and establish soundness and completeness. The paper ends with a discussion that contextualizes our current work within the broader landscape of the proof theory of relevant logics.
De Martin Polo, F. (2024) Beyond semantic pollution: Towards a practice-based philosophical analysis of labelled calculi
Erkenntnis
DOI: 10.1007/s10670-024-00823-6
[Preprint]
Abstract. This paper challenges the negative attitudes towards labelled proof systems, usually referred to as semantic pollution, by arguing that such critiques overlook the full potential of labelled calculi. The overarching objective is to develop a practice-based philosophical analysis of labelled calculi to provide insightful considerations regarding their proof-theoretic and philosophical value. To achieve this, successful applications of labelled calculi and related results will be showcased, and comparisons with other relevant works will be discussed. The paper ends by advocating for a more practice-based approach towards the philosophical understanding of proof systems and their role in structural proof theory.
De Martin Polo, F. (2023) Modular labelled calculi for relevant logics
Australasian Journal of Logic 20(1)
[PDF]
Abstract. In this article, we perform a detailed proof theoretic investigation of a wide number of relevant logics by employing the well-established methodology of labelled sequent calculi to build our intended systems. At the semantic level, we will characterise relevant logics by employing reduced Routley-Meyer models, namely, relational structures with a ternary relation between worlds along with a unique distinct element considered as the real (or actual) world. This paper realizes the idea of building a variety of modular labelled calculi by reflecting, at the syntactic level, semantic informations taken from reduced Routley-Meyer models. Central results include proofs of soundness and completeness, as well as a proof of cut- admissibility.
De Martin Polo, F. (2023) Discussive Logic. A Short History of the First Paraconsistent Logic
In: Historia Logicae. Ed. by M. Ingolf and J. Lemanski, vol. 1, College Publications, London
[Preprint]
Abstract. In this paper we present an overview, with historical and critical remarks, of two articles by S. Jaśkowski (1948 and 1949), which contain the oldest known formulation of aparaconsistent logic. Jaśkowski has built the logic – he termed discussive (D₂) – by defining two new connectives and by introducing a modal translation map from D₂ systems into Lewis’ modal logic S5. Discussive systems, for their formal details and their original philosophical justification, have attracted discrete attention among experts. Indeed, in what follows, after having introduced Jaśkowski’s methodology of building D₂ and his main philosophical motivations for providing such a system, we will explore some of the main contributions to the development of D₂.
De Martin Polo, F. (2021) A Cut-free Hypersequent Calculus for Intuitionistic Modal Logic IS5
In: Proceedings of the 18th International Workshop of Logic and Engineering of Natural Language Semantics 18, JSAI-isAI202. Ed. by A. Butler, pp. 217-230
De Martin Polo, F. (2023) Topics in the Proof Theory of Non-classical Logics. Philosophy and Applications
Ruhr University Bochum, University Library
DOI: 10.13154/294-10679
Summary. Chapter 1 constitutes an introduction to Gentzen calculi from two perspectives, logical and philosophical. It introduces the notion of generalisations of Gentzen sequent calculus and the discussion on properties that characterize good inferential systems. Among the variety of Gentzen-style sequent calculi, I divide them into two groups: syntactic and semantic generalisations. In the context of such a discussion, the inferentialist philosophy of the meaning of logical constants is introduced, and some potential objections – mainly concerning the choice of working with semantic generalizations – are addressed. Finally, I introduce the case studies that I will be dealing with in Part II. Chapter 2 is concerned with the origins and development of Jaśkowski’s discursive logic. The main idea of this chapter is to systematize the various stages of the development of discursive-logic-related research from two different angles, i.e., its connections to modal logics and its proof theory, by highlighting virtues and vices. Chapter 3 focuses on the Gentzen-style proof theory of discursive logic, by providing a characterization of it in terms of labelled sequent calculi. Chapter 4 deals with the Gentzen-style proof theory of relevant logics, again by employing the methodology of labelled sequent calculi. This time, instead of working with a single logic, I address a whole family of them. More precisely, I study, in terms of proof systems, those relevant logics that can be characterised, at the semantic level, by reduced Routley–Meyer models, i.e., relational structures with a ternary relation between states and a unique base element. Chapter 5 investigates the proof theory of a modal expansion of intuitionistic propositional logic obtained by adding an ‘actuality’ operator to the connectives. This logic was introduced also using Gentzen sequents. Unfortunately, the original proof system is not cut-free. This chapter shows how to solve this problem by moving to hypersequents. Chapter 6 concludes the investigations and discusses the future of the research presented throughout the dissertation.
Paper on bilateralism and labeled calculi (under review).
Paper on the proof theory of Jaśkowski's Discussive Logic (under review).
English translation of: Ackermann, W. (1956). Begründung einer strengen Implikation. The Journal of Symbolic Logic, 21(2): 113-128. (under review, Preprint here.)
William of Sherwood, Introductiones in logicam, Latin-to-Italian translation, with comments and introduction, 2019 (∼155 pp.)
Abstract. William of Sherwood’s 13th century logic manual, Introductiones in Logicam, was crafted as a concise volume for use during the author’s own university logic lectures. Its importance extends beyond its practical use in teaching; the text provides a clear analysis of the predominant logical questions of that era, meticulously selected and discussed in comparison to other major authors, particularly Aristotle and Boethius. Within this yet-to-be-published manuscript, I present the first Latin-to-Italian translation of Sherwood’s logic manual, Introductiones in Logicam, accompanied by comprehensive comments and a detailed historical and philosophical introduction.
De Martin Polo, F., Numbers, Objects and Abstraction. Notes on a Philosophical Interpretation of Mathematics, MA thesis, University Ca’ Foscari, Venice, 2019.
Abstract. The focus of this research lies in the philosophy of mathematics, exploring both its metaphysical and epistemological dimensions. The thesis aims to address a specific aspect of the contemporary philosophical-mathematical discourse: the possibility of admitting the existence of abstract objects in the ontology of mathematics. The inquiry centers around the mathematical Platonism articulated by K. Gödel, whose positions assert the existence of mathematical objects independently of our thoughts and propose a form of intellectual perception for knowing them. While Gödel’s stance is sophisticated, challenges have arisen, notably through the critiques of the French philosopher P. Benacerraf. Benacerraf’s theses, presented in 1965 and 1973, serve as a catalyst for scrutinizing and refining the Gödelian perspective, engaging logical, set-theoretical, and model-theoretical tools. Additionally, the work draws inspiration from the philosophical contributions of G. Frege and subsequent developments in his thought.
De Martin Polo, F., From Logic to Philosophy. Kurt Gödel’s Ontological Argument (in Italian), BA thesis, University Ca’ Foscari, Venice, 2017.
Abstract. The thesis investigates Kurt Gödel’s philosophy, focusing on his ontological argument. Part I delves into foundational debates in mathematics, covering logicism, formalism, and concluding with Gödel’s incompleteness theorems. The research explores the connection between incompleteness and the philosophy of mathematics, emphasizing Gödel’s Platonism. In Part II, the study analyzes the ontological argument, exploring its philosophical significance and contrasting Gödel’s ideas with Leibniz, Kant, and contemporary discussions on existence. The analysis sheds light on the roles of logic, metaphysics, rationalism, and phenomenology in Gödel’s philosophical observations.