On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic

Matteo Manighetti
Matteo Manighetti

TYPES, 2016.

Cited by: 0|Bibtex|Views0|Links
EI

Abstract:

Intuitionistic first-order logic extended with a restricted form of Markovu0027s 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 Markovu0027s principle. Starting from classical n...More

Code:

Data:

Your rating :
0

 

Tags
Comments