Undecidability and intuitionistic incompleteness (Q1815411): Difference between revisions

It is proved that the many-one completeness of S-derivability (for a deductive system S) and its completeness w.r.t. a class of structures K imply Markov's Principle MP (under some simple assumptions on S and K). This result yields as immediate corollary that weak completeness for classical predicate logic and strong completeness for sentential logic imply MP. Hence the corresponding completeness theorems for (the negative fragment of) intuitionistic logic (w.r.t. Beth and Kripke models) imply MP, too (and these completeness theorems are unprovable in second-order Heyting arithmetic HAS).