Talk:Markov's principle

Curry-Howard

Removed: In the Curry–Howard correspondence, Markov's principle corresponds to the termination of unbounded search. [1]

C-H is about propositions as types. The type of the unbounded search operator isn't Markov's principle. So this isn't true. Of course I sort of see where you're going, but I can't figure out how it can be reworded it to make it true. --99.245.206.188 (talk) 04:06, 4 October 2009 (UTC)

Since Markov's principle is a first order proposition, the type corresponding to it under C-H is a dependent type, namely $(\Pi x:U.P(x)+(P(x)\to \bot ))\times ((\Pi x:U.P(x)\to \bot )\to \bot )\to \Sigma x:U.P(x)$ (assuming the quantifiers range over a universe $U$). Assume $P$ is just a propositional function and has no computational content. A value of that type is a function taking as arguments 1) a proof that $P$ is decidable, whose computational content is a boolean function implementing a decision procedure for $P$; and 2) a proof that $P$ is not everywhere false, which (since it is a negation) has no computational content; and produces 1) a value $x$ of type $U$, and 2) a proof that $x$ satisfies $P$, which again has no computational content. Throwing away the first order part and leaving only the computational bits, we get the simple type $(U\to 2)\to U$, which is the type of the unbounded search operator for U (we just need to provide a decision procedure to get the least $x:U$ satisfying $P$).

This would seem to suggest that Martin-Löf type theory justifies Markov's principle. However, this would require that M-L typeability implies termination, and I'm not sure that's the case. Hairy Dude (talk) 19:24, 10 February 2010 (UTC)

Well, the type $M=\Pi f:(Nat\to 2).((\Pi n:Nat.f(n)=0)\to 0)\to \Sigma n:Nat.f(n)=1$ seems right to me (i.e U=Nat; not sure about the "general Markov's principle" proposed here). Typability does imply termination: only total functions are considered in M-L. But to say that the unbounded search operator inhabits this type begs the question. This cannot be proven in M-L anyway. There is no provision for throwing away computational content the way you describe. --Unzerlegbarkeit (talk) 22:17, 15 May 2010 (UTC)