Showing 1–3 of 3 results for author: Protin, C L

On the Various Translations between Classical, Intuitionistic and Linear Logic

Authors: Gilda Ferreira, Paulo Oliva, Clarence Lewis Protin

Abstract: Several different proof translations exist between classical and intuitionistic logic (negative translations), and intuitionistic and linear logic (Girard translations). Our aims in this paper are (1) to consider extensions of intuitionistic linear logic which correspond to each of these systems, and (2) with this common logical basis, to develop an uniform approach to devising and simplifying pro… ▽ More Several different proof translations exist between classical and intuitionistic logic (negative translations), and intuitionistic and linear logic (Girard translations). Our aims in this paper are (1) to consider extensions of intuitionistic linear logic which correspond to each of these systems, and (2) with this common logical basis, to develop an uniform approach to devising and simplifying proof translations. As we shall see, through this process of ``simplification'' we obtain most of the well-known translations in the literature. △ Less

Submitted 5 May, 2025; v1 submitted 3 September, 2024; originally announced September 2024.

MSC Class: 03F52; 03B20; 03F07; 03F25

Introduction to Pylog

Authors: Clarence Lewis Protin

Abstract: PyLog is a minimal experimental proof assistant based on linearised natural deduction for intuitionistic and classical first-order logic extended with a comprehension operator. PyLog is interesting as a tool to be used in conjunction with other more complex proof assistants and formal mathematics projects (such as Coq and Coq-based projects). Proof assistants based on dependent type theory are a… ▽ More PyLog is a minimal experimental proof assistant based on linearised natural deduction for intuitionistic and classical first-order logic extended with a comprehension operator. PyLog is interesting as a tool to be used in conjunction with other more complex proof assistants and formal mathematics projects (such as Coq and Coq-based projects). Proof assistants based on dependent type theory are at once very different and profoundly connected to the one employed by Pylog via the Curry-Howard correspondence. The Tactic system of Coq presents us with a top-down approach to proofs (finding a term inhabiting a given type via backtracking the rules, typability and type-inference being automated) whilst the classical approach of Pylog follows how mathematical proofs are usually written. Pylog should be further developed along the lines of Coq in particular through the introduction of many "micro-automatisations" and a nice IDE. △ Less

Submitted 5 June, 2023; v1 submitted 4 April, 2023; originally announced April 2023.

MSC Class: 03F03 (Primary) 03F07; 03F55; 03-04 (Secondary)

Ancient Quantifier Logic

Authors: Clarence Lewis Protin

Abstract: In this paper we argue and present evidence for the use of the natural deduction rules for universal and existential quantifiers in ancient philosophy. More specifically, we present evidence for the use and understanding of such rules for multiple quantification over non-necessarily monadic predicates and nested quantifiers over non-necessarily monadic predicates - all which amounts to the possess… ▽ More In this paper we argue and present evidence for the use of the natural deduction rules for universal and existential quantifiers in ancient philosophy. More specifically, we present evidence for the use and understanding of such rules for multiple quantification over non-necessarily monadic predicates and nested quantifiers over non-necessarily monadic predicates - all which amounts to the possession of mechanisms for dealing with multiple generality. This work aims to complement the paper by Bobzien and Shogry\cite{mult} which argues that Stoic logicians had already all the elements necessary to deal with multiple generality. While we also draw some evidence from Sextus Empiricus (a common source for Stoic logic) our focus is not on the Stoics but on logical aspects of Aristotle, Euclid, Galen and Proclus. Bobzien and Shogry argued for the ability of Stoic logic to express multiple generality through regimentation and anaphora - universal quantification is expressed by the tis + ekeinos construction on conditionals - but say relatively little about deduction rules. Our focus is on the quantifier rules themselves, specifically from the point of view of natural deduction with some incursions into dependent-type theory. This paper shares with Bobzien and Shogry the general aim of arguing for a 'somehwhat more gradual development' of the the logic of multiple generality from Aristotle to Frege. △ Less

Submitted 31 December, 2024; v1 submitted 7 September, 2022; originally announced September 2022.

Comments: The points the author desired to make in this paper have been better developed and expounded in the context of the author's other paper 'Aristotle's Second-Order Logic' [arXiv:2303.03269]