[joe_the_user]

I'm pretty sure if you are talking about proofs having to do with a determined, computation system, Godel applies.

I mean, the unsolvability of the halting problem certainly applies and this gives a somewhat similar picture of the world.

[jonsterling]

In bob's setting, the computation system is not determined or fixed. It is open-ended...

In intuitionistic mathematics, we of course accept that there is no Turing computable halting oracle, but we do not rule out the possibility that there is some other effective oracle that can decide halting. (This is in contrast to recursive mathematics / Russian constructivism)