4 papers
Peano Arithmetic and MALL
Matteo Manighetti, Dale Miller
Formal theories of arithmetic have traditionally been based on either classical or intuitionistic logic, leading to the development of Peano and Heyting arithmetic, respectively. W…
Admissible Tools in the Kitchen of Intuitionistic Logic
Andrea Condoluci, Matteo Manighetti
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 thou…
Computational Interpretations of Markov's principle
Matteo Manighetti
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 termi…
On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic
Federico Aschieri, Matteo Manighetti
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…