Lambda the Ultimate

As someone who pretty much identifies with the label "hardcore intuitionist", I have to disagree -- it's only through "hardcore intuitionism" that we find reason to seek computational meanings like this for classical reasoning. To me, axiomatic proof systems feel like "gaming the logic" more than any work along these lines.

It seems to me that any claim of the form: "I just added enough axioms from this other logic that you guys disagree with until I could prove my theorem" would qualify as 'gaming the logic' - not quite on the order of Nomic, but one is still changing the rules to fit the theorem.

As someone raised on classical logic (and who has only recently begun to appreciate constructive/intuitionist logics), I must ask: Do we have an intuitionist proof of the undecidability of the Halting problem? People who claim to be intuitionists keep bringing the Halting problem up in their arguments, so I'm curious.

But haven't really had time to work out the argument. Can you write down what the intuitionist argument is?

[I guess it is stated in the original post. Can someone explain what: "It depends" means?]

...of the halting theorem is a perfectly good constructive proof. You assume that you have a halting oracle, and then explicitly construct an input to this oracle which leads to absurd results, from which you conclude that no such oracle exists.[*]

This has no connection to the "it depends" in my original post. That is just a reference to the fact that there are many different models of intuitionistic logic, and Markov's principle is inconsistent with some of them. So whether you accept it depends on what you need to do.

[*] If you think this sounds like a proof by contradiction, you should read the following post by Andrej Bauer, which he wrote to explain the distinction between proofs of negative statements and proofs by contradiction to Timothy Gowers(!!!).

So, I am a sceptic and am gonna do some nitpicking: Why is a program which loops forever partial?

Thanks for that insight, esp. the link to Andrej Bauer's post.

I believe that the "usual" proof of the undecidability of the halting problem is formalisable in intuitionnistic Heyting Arithmetic. Remember that proof by contradiction is allowed for negative statements in intuitionnistic logic, it is only the use of contraposition that is suspect.

As per your other comment, I believe that the argument is not so much about Hard Core intuitionnnists versus classical logic proponents (classisists?) but more about what computationnal content one can extract from proofs in such a logic. It is interesting to note that many proofs in ordinary classical logics (in fact, all the \Pi^0_1 statements) have a strong computationnal content with, for example the witness property. This paper proposes a refinement of these kind of statements. The title is just to attract attention...

It seems a lot like gaming the logic.

There's nothing hardcore about my intuitionism —I'm a "semantic intuitionist", which means I think semantics should be done in a rigorously constructive fashion, but I don't have hangups about, say the consistency or use of ZFC+(regular cardinals), and I don't tell mathematicians that what they do is incorrect— but I think this is too much for any but the most paranoid ultra-finitist.

Gödel's Dialectica interpretation shows how all theorems of Peano arithmetic cleanly match theorems of Heyting arithemtic in such a way that we see that the Pi-0-2 theory of classical and intuitionistic arithmetic are the same. Fernando Ferreira (2008, A most artistic package of a jumble of ideas, Dialectica 62-2) shows how we can view this as a constructive interpretation of Markov's principle.

I had assumed that was P ranging over decidable predicates, but if you want to make that assumption explicit then the way you wrote it is exactly right. You're also correct that Markov's principle allows a limited form of double negation elimination: if you write it as (¬¬∃x. P(x)) → ∃x. P(x) (for decidable P), then it is very clear.

(I wrote it the other way around because I thought it made the idea that it licenses you to use nonconstructive termination proofs a bit clearer. Herbelin gives it in the double-negation-elimination form in his introduction, to make the connections with call/cc clearer. I think it would be nice to study his translation more carefully, to see exactly how these two perspectives connect.)

"Wouldn't it need to be ((∀x. P(x) \/ ¬P(x)) /\ ¬(∀x. ¬P(x))) → ∃x. P(x)?"

Whoa! Doesn't
1. ∀x. P(x) \/ ¬P(x) reduce to
2. ∀x. true which reduces to
3. true

I can "and" any number of true statements to any statement whatsoever without altering the overall expression's truth value. Isn't that what you've done here? What's gained?

Intuitionist logics are effectively classical logic without the law of the excluded middle. You cannot say P(x) just because you can prove ¬¬P(x). That is, you say P(x) because you can directly (constructively) prove P(x).

Thus ∀x. P(x) \/ ¬P(x) is a non-trivial statement that you can prove P(x) or you can prove ¬P(x) for any given x - which is, essentially, to say that P(x) is decidable. (For example, you couldn't replace P with "does this program halt?" because a "Halts(program)" predicate is not generally decidable.)

I'd assume an extra requirement that 'x' be from a countable set. But I'm not well enough versed in intuitionist logics to know whether that countability is traditionally implied.

The formulation of Markov principle described here requires finite but unbounded search (P(x) because I can prove P(x) if given finite unbounded search). Is this acceptable? Well, as the OP says, "it depends" - apparently upon the mathematician and upon the problem.

I'd assume an extra requirement that 'x' be from a countable set. But I'm not well enough versed in intuitionist logics to know whether that countability is traditionally implied.

You can do mathematics with intuitionistic logic and uncountable sets, but it's not constructive anymore. Also, you really need something more than countability: you need to have some kind of structure you can recurse over.

The original statement of Markov's principle of constructive choice is, I understand, from A. A. Markov, 1954, Theory of algorithms, and is formulated with quantification over the natural numbers. Markov's book is a goldmine of thinking about what algorithms are, and what it means for mathematics to be algorithmic.

The usefulness of Markov's principle in constructive analysis is what has led to more liberal versions of Markov's principle.

(For example, you couldn't replace P with "does this program halt?" because a "Halts(program)" predicate is not generally decidable.)

In fact, Markov's principle in essence says that there is a fact of the matter about whether a program halts, something about which purer forms of intuitionism are agnostic.

Markov's principle in essence says that there is a fact of the matter about whether a program halts or not, something about which purer forms of intuitionism are agnostic.

Could you explain this? Does it have something to do with step-wise decidability of halting? Could I replace 'P' with 'Halts'?

Does it have something to do with step-wise decidability of halting?

If you like — actually that's a nice phrase for this kind of thing. For any program e, let E(n) be the predicate that says e halts at the nth step. Then I think it is clear how to get your result from Markov's principle.

Could I replace 'P' with 'Halts'?

No, because Halts(-) is not a decidable predicate. Markov's principle doesn't tell you whether the existential is true or not, only that there is no excluded middle between it being true and it being false.