arXiv subjects

Clarence Lewis Protin

Publications and source records attributed to Clarence Lewis Protin.

3 recordsLinked to original sources

arXiv2026

Quantifier Reasoning and Multiple Generality in Aristotle and Ancient Logic

Aristotelian logic and its related traditions in antiquity are often held to have been equivalent to monadic predicate logic and as such inadequate to formalize mathematics as well as scientific and philosophical discourse in general. In this paper we argue that on the contrary the logical theories of Aristotle and ancient authors such as Galen and Boethius were in fact quite sufficient to account for the logically complex expressions and reasoning involving multiple generality fundamental to the aforementioned disciplines.

math.LO↗

arXiv2025

On the Various Translations between Classical, Intuitionistic and Linear Logic

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 a 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.

math.LO↗

arXiv2023

Introduction to Pylog

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.

math.LO↗