-
Peano Arithmetic and $μ$MALL
Authors:
Matteo Manighetti,
Dale Miller
Abstract:
Formal theories of arithmetic have traditionally been based on either classical or intuitionistic logic, leading to the development of Peano and Heyting arithmetic, respectively. We propose a use $μ$MALL as a formal theory of arithmetic based on linear logic. This formal system is presented as a sequent calculus proof system that extends the standard proof system for multiplicative-additive linear…
▽ More
Formal theories of arithmetic have traditionally been based on either classical or intuitionistic logic, leading to the development of Peano and Heyting arithmetic, respectively. We propose a use $μ$MALL as a formal theory of arithmetic based on linear logic. This formal system is presented as a sequent calculus proof system that extends the standard proof system for multiplicative-additive linear logic (MALL) with the addition of the logical connectives universal and existential quantifiers (first-order quantifiers), term equality and non-equality, and the least and greatest fixed point operators. We first demonstrate how functions defined using $μ$MALL relational specifications can be computed using a simple proof search algorithm. By incorporating weakening and contraction into $μ$MALL, we obtain $μ$LK+, a natural candidate for a classical sequent calculus for arithmetic. While important proof theory results are still lacking for $μ$LK+ (including cut-elimination and the completeness of focusing), we prove that $μ$LK+ is consistent and that it contains Peano arithmetic. We also prove two conservativity results regarding $μ$LK+ over $μ$MALL.
△ Less
Submitted 21 December, 2023;
originally announced December 2023.
-
Admissible Tools in the Kitchen of Intuitionistic Logic
Authors:
Andrea Condoluci,
Matteo Manighetti
Abstract:
The usual reading of logical implication "A implies B" as "if A then B" fails in intuitionistic logic: there are formulas A and B such that "A implies B" is not provable, even though B is provable whenever A is provable. Intuitionistic rules apparently do not capture interesting meta-properties of the logic and, from a computational perspective, the programs corresponding to intuitionistic proofs…
▽ More
The usual reading of logical implication "A implies B" as "if A then B" fails in intuitionistic logic: there are formulas A and B such that "A implies B" is not provable, even though B is provable whenever A is provable. Intuitionistic rules apparently do not capture interesting meta-properties of the logic and, from a computational perspective, the programs corresponding to intuitionistic proofs are not powerful enough. Such non-provable implications are nevertheless admissible, and we study their behavior by means of a proof term assignment and related rules of reduction. We introduce V, a calculus that is able to represent admissible inferences, while remaining in the intuitionistic world by having normal forms that are just intuitionistic terms. We then extend intuitionistic logic with principles corresponding to admissible rules. As an example, we consider the Kreisel-Putnam logic KP, for which we prove the strong normalization and the disjunction property through our term assignment. This is our first step in understanding the essence of admissible rules for intuitionistic logic.
△ Less
Submitted 16 October, 2018;
originally announced October 2018.
-
On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic
Authors:
Federico Aschieri,
Matteo Manighetti
Abstract:
Intuitionistic first-order logic extended with a restricted form of Markov's principle is constructive and admits a Curry-Howard correspondence, as shown by Herbelin. We provide a simpler proof of that result and then we study intuitionistic first-order logic extended with unrestricted Markov's principle. Starting from classical natural deduction, we restrict the excluded middle and we obtain a na…
▽ More
Intuitionistic first-order logic extended with a restricted form of Markov's principle is constructive and admits a Curry-Howard correspondence, as shown by Herbelin. We provide a simpler proof of that result and then we study intuitionistic first-order logic extended with unrestricted Markov's principle. Starting from classical natural deduction, we restrict the excluded middle and we obtain a natural deduction system and a parallel Curry-Howard isomorphism for the logic. We show that proof terms for existentially quantified formulas reduce to a list of individual terms representing all possible witnesses. As corollary, we derive that the logic is Herbrand constructive: whenever it proves any existential formula, it proves also an Herbrand disjunction for the formula. Finally, using the techniques just introduced, we also provide a new computational interpretation of Arithmetic with Markov's principle.
△ Less
Submitted 17 October, 2017; v1 submitted 16 December, 2016;
originally announced December 2016.
-
Computational Interpretations of Markov's principle
Authors:
Matteo Manighetti
Abstract:
Markov's principle is a statement that originated in the Russian school of Constructive Mathematics and stated originally that "if it is impossible that an algorithm does not terminate, then it will terminate". This principle has been adapted to many different contexts, and in particular we are interested in its most common version for arithmetic, which can be stated as "given a total recursive fu…
▽ More
Markov's principle is a statement that originated in the Russian school of Constructive Mathematics and stated originally that "if it is impossible that an algorithm does not terminate, then it will terminate". This principle has been adapted to many different contexts, and in particular we are interested in its most common version for arithmetic, which can be stated as "given a total recursive function f , if it is impossible that there is no n for which f(n) = 0, then there exists an n such that f(n) = 0". This is in general not accepted in constructivism, where stating an existential statement requires one to be able to show at request a witness for the statement: here there is no clear way to choose such an n. We introduce more in detail the context of constructive mathematics from different points of view, and we show how they are related to Markov's principle. In particular, several realizability semantics are presented, which provide interpretations of logical systems by means of different computational concepts (mainly, recursive functions and lambda calculi). This field of research gave origin to the well known paradigm often called Curry-Howrd isomorphism, or also propositions as types, that states a correspondence between proofs in logic and programs in computer science. Thanks to this the field of proof theory, that is the metamathematical investigations of proofs as mathematical objects, became of interest for computer science and in particular for the study of programming languages. By using modern research on the Curry-Howard isomorphism, we will obtain a more refined interpretation of Markov's principle. We will then use this results to investigate the logical properties of systems related to the principle, and introduce a proof transformation technique to interpret constructively some non-constructive proofs of arithmetic.
△ Less
Submitted 16 December, 2016; v1 submitted 11 November, 2016;
originally announced November 2016.
