There are some who hold that a statement that is unprovable within a deductive system may be quite provable in a metalanguage. And what cannot be proven in that metalanguage can likely be proven in a meta-metalanguage, recursively, ad infinitum, in principle. By invoking such a system of typed metalanguages, along with an axiom of Reducibility — which by an inductive assumption applies to the entire stack of languages — one may, for all practical purposes, overcome the obstacle of incompleteness.
>>8 The same way Gödel's theorem is useful in the real world.
yes it is [spoiler[(if you're a proof theorist)[/spoiler]
Name:
Anonymous2009-04-25 8:47
oh god what I have done
Name:
Anonymous2009-04-25 10:56
oh godel what I have done I don't even
Name:
Anonymous2009-04-25 11:33
>>4
That's bullshite. By metalanguage they usually mean just your initial language plus an additional axiom that says that your unprovable statement is, in fact, true. Or false, you will not have a contradiction either way. What's the point?
It's even more blatantly stupid when rephrased in the Halting Problem framework: so, you have found an undecidable program - i.e. one that can't be proven neither to halt nor not to halt. "Constructing a metalanguage" now means defining a new evaluator that is able to recognize this specific program and halt. Or go into the infinite loop, if you feel like it. And so you are magically able to solve a halting problem for this concrete program in your new shiny meta-evaluator - now you definetly know that it would halt (or not) and pre-analyze the program yourself and output just that if it was recognized. Wow, isn't that useful? A great success if you ask me!
Name:
Anonymous2009-04-25 11:47
>>13
Yeah, theoretical CS is a truckload of bulls.
>>13,14 theoretical CS is a truckload of bulls
Oh my!. A theoretical topic with no practical applications!? We should travel back in time and destroy all of formal logic in the ninteen and twentieth centuries, because in a similar fashion, it has stopped people working on things with real world applications.
Name:
Anonymous2009-04-25 13:34
>>15
Did I say anything about other fields? Theoretical CS is shit and shouldn't be discussed here... oh wait /prog/ loves jerking over useless concepts like SICPs and the Sage Monad.
Name:
Anonymous2009-04-25 13:42
>>14 theoretical CS is a truckload of bulls
What are you referring to? can you name some authors for example?