if (DoesItHalt() == True)
while(True) // loop forever
;
else if (DoesItHalt() == False)
return False;
else if (DoesItHalt() == NeitherTrueNorFalse)
return NeitherTrueNorFalse;
So the original Halting Problem was incorrectly formed specifically
because it was framed as a Boolean function, thus failing to account
for possible inputs that result in a reply other than True or False.
How do you tell the set NeitherTrueNorFalse from the set False?
What would that mean, with respect to the TM operations, to say
that DoesItHalt() == NeitherTrueNorFalse
if (DoesItHalt() == True)
while(True) // loop forever
;
else if (DoesItHalt() == False)
return False;
else
return NeitherTrueNorFalse;
Not sure how that helps.
Function DoesItHalt(Machine m, Input i) returns Tristate;
Procedure MrProblem(Input i)
{
Machine m = (Machine) i;
while(DoesItHalt(m, i) == True)
;
}
begin
writeln(DoesItHalt(MrProblem, MrProblem))
end.
What does this program output?
1. True. In which case we have an immediate contradiction.
2. False. In which case we also have an immediate contradiction.
3. NeitherTrueNorFalse. In which case MrProblem provably halts.
Another contradiction.
Perhaps the best response is to convert DoesItHalt() into an
incomplete problem by returning IHaveNoIdea. :-) That way,
DoesItHalt() can apply various heuristics and be an implementable,
if incomplete, function.
--
#191, ewi...@earthlink.net
It's still legal to go .sigless.
>>
>> else if (DoesItHalt() == NeitherTrueNorFalse)
>> return <whatever>;
>>
What do you mean by "NeitherTrueNorFalse"?
I mean we have:
(a) "DoesItHalt()" is True IFF if the program halts.
(b) "DoesItHalt()" is False IFF if the program doesn't halt.
Now is there a THIRD state of the program besides (a) halt and (b)
doesn't halt (loop)? Which one? The crackpot state?
F.
Peter Olcott wrote:
>>>
>>> else if (DoesItHalt() == NeitherTrueNorFalse)
>>> return <whatever>;
>>>
What do you mean by "NeitherTrueNorFalse"?
I mean we have:
(a) "DoesItHalt()" is True iff the program halts.
(b) "DoesItHalt()" is False iff the program doesn't halt.
Case of the crackkettle calling the crackpot black!
Herc
Seemingly his machine is broken. Having had some experience looking for
Turing machine parts, I'd advised him first to take his machine to a
psychic surgeon and have the defective parts removed. Then he'd know what
parts to replace.
Apparently |-|erc is looking for a third state in his halting test.
Not unreasonable if done right -- I'd advocate a "IHaveNoIdea"
return state, which basically means the heuristics in the
testing procedure failed; there's no contradiction that way -- but
I don't think |-|erc's done it quite right here. :-)
Peter!
Since the output should be deterministic, and we want it to output "halts" for
all halting programs atleast some of the time, how about a parameter for depth
of search.
Halt(function, param, cycles) =
1, halted
2, still running
3, crashed
This should be programmable using a UTM that is recalled from emulating
the function after cycles cycles.
Halt(function, param, cycles) {
dummy = nul
for (cycleno = 1, cycleno < cycles, cycleno++) {
dummy = sUTM(function, param)
}
if (dummy == nul) {
return stillrunning
}
elseif (dummy = "error") {
return crashed
}
else {
return halted
}
sUTM does 1 or a few cycles at a time, it remembers where it was up to,
or we can call it in increasing cycle amounts.
Thats a basic 3 state Halt program, the question is can you get its complexity
below the complexity of the function its testing? i.e. to be useful you have
to ditch UTM and use some other method that saves time. If you can figure
out in x^2 time that a e^x function f(x) halts then its very useful.
Does your tristate proof disprove such a program?
Herc
And then what exactly happens when the original Halt function
is fed an English Poem as its input data? Does the English Poem
Halt? Does it not Halt? Perhaps it is Neither!
If we really wanted to take this to its limits it would not be constrained
at all. Since the Halting problem is proposed to place an absolute limit
on the potential for artificial intelligence, it should be free to respond
in
any way that is appropriate. When fed an English Poem, it would then
respond: This is not a computer program, it is an English Poem. It could
then go on to critique the quality of the poem, and perhaps chastise the
one whom submitted it to evaluate whether or not it would halt. Nothing
about either the Incompleteness Theorem or the Halting Problem would
limit its capability to do this.
>> >One very simple transformation of the problem into a solvable problem
>> >is to convert the Boolean function DoesItHalt() into a tertiary response:
>> >True, False, Neither.
>> >if (DoesItHalt() == True)
>> > while(True) // loop forever
>> > ;
>> >else if (DoesItHalt() == False)
>> > return False;
>> >else if (DoesItHalt() == NeitherTrueNorFalse)
>> > return NeitherTrueNorFalse;
>> >So the original Halting Problem was incorrectly formed specifically
>> >because it was framed as a Boolean function, thus failing to account
>> >for possible inputs that result in a reply other than True or False.
>> What would that mean, with respect to the TM operations, to say
>> that DoesItHalt() == NeitherTrueNorFalse
>If the input data is an English poem, (or any other invalid input) the
>Halt() function returns that it neither halts, nor does not halt.
By definition of the Turing Machine, there is no such thing as
"invalid input".
the question remains, what will a computer do when it runs the data, function or poem?
return from processing ready for its next command, or get tied up into an infinite loop
somewhere. people used to hack computers like this, some early programs inputed
something from the user into a textbox, and the part of memory allocated to the text
box was in the module that parsed it. so they allocated 100 chars of memory to input
the text, then after that section in memory was the code to parse it. So hackers typed
over 100 characters, and the extra characters they typed overwrote the original program
and they issued it instructions to give the user control of the computer.. actually similar
techniques still going around on the web.
so even if its a poem, that poem can be indexed as a big number identifying it. and even
it doesn't make sense to get a computer to run it it still can.
the problem splits down into this subproblem :
how do you tell the input is a poem and not a program?
once you have a systematic technique to determine a program, then the
2 value halting program applies to that, and a contradiction will still ensue.
Herc
>
> Apparently |-|erc is looking for a third state in his halting test.
> Not unreasonable if done right -- I'd advocate a "IHaveNoIdea"
> return state...
>
But that too would mean that the Halting Problem is not solved. No? :-)
(Right: No surprise, since we know that it is not solvable.)
F.
Curious how you never actually reply to objections.
As I pointed out elsewhere, requiring the program to respond to
"invalid input" is simply changing the problem - it's hard to
see what your comments about this new problem have to do with
the original problem.
And second, the new problem,
(*) reply correctly 'InvalidInput', 'ValidInputThatHalts',
or 'ValidInputThatDoesNotHalt', regardless of the input.
is easily seen to be just as unsolvable as the actual halting
problem: a program that does (*) _also_ solves the actual
halting problem "reply correctly Halts or DoesNotHalt, given
any valid input"!
It's incredibly hard to see what you think you've accomplished
by modifying the problem to (*), since it's so obvious that
any program that does (*) suffices as a solution to the
standard halting problem.
>If we really wanted to take this to its limits it would not be constrained
>at all. Since the Halting problem is proposed to place an absolute limit
>on the potential for artificial intelligence, it should be free to respond
>in
>any way that is appropriate. When fed an English Poem, it would then
>respond: This is not a computer program, it is an English Poem. It could
>then go on to critique the quality of the poem, and perhaps chastise the
>one whom submitted it to evaluate whether or not it would halt. Nothing
>about either the Incompleteness Theorem or the Halting Problem would
>limit its capability to do this.
>
************************
David C. Ullrich
That's a different problem. That's not "will it halt?".
That's "will it halt within a fixed number of cycles?".
Also, TM's don't crash. :-)
No, it does not disprove such a program. A fixed-cycle halter
is easy to write -- just run the simulated TM for that number
of cycles.
> "Neil W Rickert" <ricke...@cs.niu.edu> wrote in message
> news:c9v9fp$q5h$1...@usenet.cso.niu.edu...
>
>>"Peter Olcott" <olc...@worldnet.att.net> writes:
>>
>>
>>>One very simple transformation of the problem into a solvable problem
>>>is to convert the Boolean function DoesItHalt() into a tertiary response:
>>>True, False, Neither.
>>
>>>if (DoesItHalt() == True)
>>> while(True) // loop forever
>>> ;
>>>else if (DoesItHalt() == False)
>>> return False;
>>
>>>else if (DoesItHalt() == NeitherTrueNorFalse)
>>> return NeitherTrueNorFalse;
>>
>>>So the original Halting Problem was incorrectly formed specifically
>>>because it was framed as a Boolean function, thus failing to account
>>>for possible inputs that result in a reply other than True or False.
>>
>>What would that mean, with respect to the TM operations, to say
>>that DoesItHalt() == NeitherTrueNorFalse
>>
>
> If the input data is an English poem, (or any other invalid input) the
> Halt() function returns that it neither halts, nor does not halt.
Since a TM is normally defined to read a very restricted set of input
(blank/not-blank), it will interpret the English poem the same as the
unary string that is equivalent to it.
Put another way, what makes you think you can input an English poem?
This sounds like you are wending your way into the ridiculous to get
around something you don't like.
> What
> is implied (logically entailed, in a sense) when the program reports
> either true or false, is that "the computer program halts" or "the
> computer program does not halt". Thus when it is fed data that is
> not a computer program, it can not correctly respond with either
> true or false.
It will interpret it as a computer program and work accordingly. The
input is a number. The number will be interpretted, decoded, etc. It
is not fed a program.
> If it is constrained to respond with only the two choices
> of true or false, then it is formed erroneously.
No, your understanding of how it works is erroneous.
> If we really wanted to take this to its limits it would not be constrained
> at all. Since the Halting problem is proposed to place an absolute limit
> on the potential for artificial intelligence, it should be free to respond
> in
> any way that is appropriate. When fed an English Poem, it would then
> respond: This is not a computer program, it is an English Poem. It could
> then go on to critique the quality of the poem, and perhaps chastise the
> one whom submitted it to evaluate whether or not it would halt. Nothing
> about either the Incompleteness Theorem or the Halting Problem would
> limit its capability to do this.
You can make TM's that will read in a Godel encoding of an English Poem
and respond with another number which signifies that. This would not
the halting TM or how it interprets that same number, since it will
interpret the input as using a Godel numbering of programs.
Quick hint: when you change the nature of the system (such as what is
output), you are likely to also find different results from the original
system. This does not indicate a flaw in the original system, only that
your new system does not necessarily correctly represent the old one.
--
Will Twentyman
email: wtwentyman at copper dot net
ok, take standard 2 parameters, function and parameter,
and have 5 different halting programs.
haltlinear (f, p)
cycles = 1,000,000 * p
...
haltpolyl (f, p)
cycles = 1,000,000 *p*p
haltpolyh (f, p)
cycles = 1,000,000 *p^100
haltexp (f, p)
cycles = 1,000,000 * e^p
like so. Now we have a bona fide halt program that categorises the
function into what class it belongs to, by giving an upper bound to the
number of cycles for programs in that class.
useful no?
>
> Also, TM's don't crash. :-)
do so.
>
> No, it does not disprove such a program. A fixed-cycle halter
> is easy to write -- just run the simulated TM for that number
> of cycles.
not the program I was talking about, can you solve an exponential program
in polynomial time. i.e. is there a haltexp that halts in polynomial time (a fixed
cycle halter using a simple type of emulator wont work).
Herc
Then how is it that this "Turing Machine" is not ill-conceived?
What does a Boolean function do when the result does not fir
into true and false?
Perhaps the original problem is a form of invalid input?
The point of the Turing Machine is that anything computable can be
represented by it. Also Blank/Not Blank would be binary, and not
unary.
I though of that option too. One could interpret this as unsolved, and
unsolvable. Yet some sort of third state would be required for any
form of invalid input, such as feeding an English Poem to a Boolean
function that is to determine whether or not a computer program will
halt. Here I will state my proposal succinctly:
The only reason that the Halting problem is unsolvable is because
the problem itself forms an absurdity.
"Peter Olcott" <olc...@worldnet.att.net> writes:
>> >If the input data is an English poem, (or any other invalid input) the
>> >Halt() function returns that it neither halts, nor does not halt.
>> By definition of the Turing Machine, there is no such thing as
>> "invalid input".
>Then how is it that this "Turing Machine" is not ill-conceived?
I suggest that you lookup the definition of a Turing machine.
>What does a Boolean function do when the result does not fir
>into true and false?
The TM makes internal state changes, and writes marks to its tape,
based on the what is already on the tape. Evaluating a Boolean
function is not part of its definition.
If you want to invent an Olcott machine that works differently, it is
your right to do so. But what happens on your Olcott machine would
have no relevance to Turing's Halting Problem, since that is for
Turing machines, not for Olcott machines.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.2.4 (SunOS)
iD8DBQFAxQbevmGe70vHPUMRAh2HAKCHKdoDoGKEglx36fA9H8+2FZ3i/QCeNyFc
+8Di1nvJWJNqHzyxjsFiWtM=
=Q7Z+
-----END PGP SIGNATURE-----
Oh Yeah, that's what I thought. I would not construe this to mean
that there is no such thing as Invalid Input on a Turing Machine.
What would be more accurate statement would be to say that a
Turing Machine is a fundamental automaton, whereby concepts
such as "Invalid Input" are not directly represented, yet could be
represented at a higher level abstraction.
Any system that is sophisticated enough to determine whether or
not most any program would halt, would require these higher level
abstractions, even though the ultimate representation of these higher
level abstractions is at a much lower level.
can you define boolean Halt in terms of your ternary Halt?
function Halt (program, parameter) {
if (Halt3(program, parameter) = "halts") return 1
if (Halt3(program, parameter) = "notdefined") return 1
if (Halt3(program, parameter) = "loops") return 0
}
If so the contradiction can still be made.
Another way is to test every program with Halt3 and make sure its defined.
Then we restrict the halting proof to all the defined functions.
As long as there are defined functions to work on, the halting proof works.
Herc
No.
Peter, you are doing something very, very strange. On the one
hand, you say you don't want to know the nitty-gritty details
of Turing's proof or Godel's proof. You just want to know an
intuitive, informal description. On the other hand, your comments
are all nit-picks about the details. And the details are exactly
what you *can't* get from an informal description. So your efforts
to attack these theorems based on informal presentations are a
complete and utter waste of time.
They wouldn't be a waste of a time if you had the ability to
see which details are unimportant, and which are critical, but
you have an uncanny ability to home in on the most trivial,
irrelevant aspect of any problem.
--
Daryl McCullough
Ithaca, NY
This curious pathology, so robustly in evidence here, has been astutely
characterized in general in another forum as the "inability to
distinguish mathematics from the contents of one's own imagination."
-cm
The "Halting Problem" is another mere absurdity, like the "Barber Paradox".
It is only unsolvable, specially because it was defined to be unsolvable.
It places no limits on the eventual capabilities of Artificial Intelligence,
even
though many claim that it does.
If (DoesTheProgramHalt == true) return 1;
else if DoesTheProgramHalt == false) return 0;
else return -1; // The Program NeitherHaltsNoDoesNotHalt
Think about this for a few hundred more hours, and then get back to me.
The ONLY reason that the {Halting Problem} is unsolvable is because
it was specifically defined to be unsolvable. It was made unsolvable by
(in a sense) being forced to produce a contradiction. Everyone that knows
logic, knows that any contradiction is complete proof of unsound reasoning.
(Anyone that does not know this, merely presumes to know logic).
Ah so you are saying that the {Halting Problem} was NOT formed
to produce a contradiction?
if (Halts(Program))
while(true); // loop forever
>
> If (DoesTheProgramHalt == true) return 1;
> else if (DoesTheProgramHalt == false) return 0;
> else return -1 // The Program NeitherHaltsNoDoesNotHalt
>
Since any TM _either_ halts (DoesTheProgramHalt == true) _or_ does not
halt (DoesTheProgramHalt == false), the else clause well never be
reached.
Moreover what does the following program do (if supplied as it's own
input):
If (DoesTheProgramHalt(input,input) == true) loop;
else if (DoesTheProgramHalt(input,input) == false) stop;
else stop;
F.
Nonsense. Termination analysis is a vital part of any decent
compiler, and it would be absolutely essential if it weren't for
the unsolvability of the halting problem.
Not to speak of all the other problems like algorithm equivalence
which might become decidable with the mathematical breakthrough
lurking behind your implication that there might be a formulation
of the halting problem which is decidable and still general enough
to cover every Turing-equivalent computation procedure.
So, if you know a way of formulating the problem of deciding whether
or not an arbitrarily given computation procedure will terminate on
every input in such a way that it is not "specifically defined to be
unsolvable", come forward with it immediately!
regards
Stephan
> Think about this for a few hundred more hours, and then get back to me.
> The ONLY reason that the {Halting Problem} is unsolvable is because
> it was specifically defined to be unsolvable.
Of course it was. Its sole purpose was to show that there are problems
which are unsolvable. What exactly is the problem? (You seem to claim
the same thing as everybody else, but in a slightly different terminology.)
> It was made unsolvable by
> (in a sense) being forced to produce a contradiction.
Assuming that the halting problem is solvable leads to a contradiction, yes.
> Everyone that knows
> logic, knows that any contradiction is complete proof of unsound reasoning.
Not true. If you prove a contradiction, then you must conclude that one
of the premises is false. This is completely sound reasoning. And this
is exactly how the proof of the unsolvability of the halting problem works:
(1) ASSUME halting problem is solvable
(2) this leads to a CONTRADICTION
(3) THEREFORE halting problem is NOT solvable
But you know this already, of course. So maybe this is merely a
misunderstanding, in the sense that one of us is using nonstandard
terminology to refer to standard and well-known things.
groente
-- Sander
That's a line of logic I followed. If you define all programs to halt then the
halt program is just TRUE.
Here's an analogy to the halting problem, to give some scope of what types of
*diagnosis are impossible.*
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Nanotechnology has prevailed, the human race is strong and healthy
and live as immortals.
A popular sport is the marathon club. Each day millions of runners
get up in the morning, run their hearts out, have a break, run again
during the day, all day every day. As immortals they apparently run
forever, but occasionaly some will quit from the club for one reason
or another. Every marathon runner is given a top with his unique
number printed on it, maybe one day to feature on the 6:02 pm
sports break broadcast on www.YeOldeCoffeeShoppe.com.
Doctor Health was concerned about the runners giving up, so he devised
a medical test to determine which runners will keep running forever and
which runners will stop. After he examines the runners he places one of 2
stickers on their gernsey HALT or RUN, so each runner knows if they would
last forever doing marathon runs. This was great, it reduced the stress of
long term members leaving and everyone was happy. The test was perfect,
every runner with RUN on their gernsey was still in the marathon club, only
people diagnosed with HALT ever left.
Doctor Health obtained a lot of notoriety having his perfect diagnosis record,
then one day an Australian joined the marathon club, from down under...
Being new, the Australian was given the task of washing the gernseys every
Saturday. He wasn't happy with this, so he decided if the last gernsey
he pulled out from the wash has a RUN sticker on it, he would give up marathon
running. If the sticker was a HALT, he would keep running. Weeks went by
and for a while every last gernsey he pulled from the wash was HALT so he
endured the washing duties. Then one week, he was extra tired from a large
marathon that day, he pulled out the last gernsey anxious to see what he should
do. To his suprise the gernsey was #475468 HIS OWN GERNSEY!!
Does the Australian marathon runner keep running the next week or give up?
How does this affect Doctor Health's diagnosis rate?
Herc
If you define all numbers to be prime, the Goldbach conjecture follows
easily. Now that I've got the knack for your style of mathematics, I see
its inherent superiority.
--
Aatu Koskensilta (aatu.kos...@xortec.fi)
"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
I thought you had work to do?
Right, if you came up with a godel numbering scheme where all n in N represented
halting programs and that subset of TMs was equivalent in computing power to
other systems of programs.... then Halt is definable (as True) and the harness that
goes into an infinite loop deliberately will not qualify as a valid program. No contradiction.
Its not exactly like ignoring composite numbers. The halt function is designed to find
programs that work, and has the assumption that some programs don't work. I just
removed that assumption. There's lot of website builders coming out now that make
large programs of perfect code, macro makers in database builders, what limitation do
they have theoretically?
Herc
> I thought you had work to do?
What makes you think that? Anyways, useless news blathering can be more
entertaining than work.
> Right, if you came up with a godel numbering scheme where all n in N represented
> halting programs and that subset of TMs was equivalent in computing power to
> other systems of programs.... then Halt is definable (as True) and the harness that
> goes into an infinite loop deliberately will not qualify as a valid program. No contradiction.
My, you have just demonstrated that the halting problem for total
recursive functions is solvable! That would be a major theoretical
breaktrough, if it weren't for the fact that everyone knows this already.
As to coming "up with a godel numbering scheme where all n in N
represented halting programs and that subset of TMs was equivalent in
computing power to other systems of programs", it's my sad duty to
inform that any such numbering must be non-effective. If you think
otherwise, please actually provide such a numbering. Adding "axioms" to
that effect will not do anything for anyone interested in computing,
anymore than adding an "axiom" that every "truth is provable" will help
anyone in proving anything.
I thought usenet was just your escape from actual work?
>
> > Right, if you came up with a godel numbering scheme where all n in N represented
> > halting programs and that subset of TMs was equivalent in computing power to
> > other systems of programs.... then Halt is definable (as True) and the harness that
> > goes into an infinite loop deliberately will not qualify as a valid program. No contradiction.
>
> My, you have just demonstrated that the halting problem for total
> recursive functions is solvable! That would be a major theoretical
> breaktrough, if it weren't for the fact that everyone knows this already.
>
> As to coming "up with a godel numbering scheme where all n in N
> represented halting programs and that subset of TMs was equivalent in
> computing power to other systems of programs", it's my sad duty to
> inform that any such numbering must be non-effective. If you think
> otherwise, please actually provide such a numbering. Adding "axioms" to
> that effect will not do anything for anyone interested in computing,
> anymore than adding an "axiom" that every "truth is provable" will help
> anyone in proving anything.
IOW, it can't be done because you haven't done it yet. Impressive, no wonder
you choose to believe the truth of things without any proof.
Herc
All these perhap's and if's are silly. It's like I'm posting
on sci.astronomy, explaining that perhaps the moon is made
of green cheese.
Exactly what _is_ invalid about "Does there exist a Turing
machine which will determine whether or not another Turing
machine halts with a certain input?"
************************
David C. Ullrich
> I thought usenet was just your escape from actual work?
I'm not being held captive here.
> IOW, it can't be done because you haven't done it yet. Impressive, no wonder
> you choose to believe the truth of things without any proof.
No, it can't be done due to simple facts from recursion theory you
choose to ignore. You make wild claims and when asked to actually
provide the constructions you claim to exist you reply by making claims
about my behaviour.
The proof are all there in numerous books and publications on recursion
theory. There can't be an effective indexing of all total recursive
functions, because you can't effectively decide for a partial recursive
function whether or not it's total.
IOW there is no halt function. I know the half dozen incomputable proofs all
have 5 variants in other domains and nobody has to defend them they can just
call upon a different version when questioned. And all the noncomputable proofs
support one another, so its not 1 proof I have to find a flaw, its all 30.
Now why do you accept "this statement G has no proof" over "proof(x)<->x".
They're just mutually exclusive, both of them appear as formula in formal systems
did G come 1st? How do you prove x without proof(x)?
Herc
> Now why do you accept "this statement G has no proof" over "proof(x)<->x".
> They're just mutually exclusive, both of them appear as formula in formal systems
> did G come 1st? How do you prove x without proof(x)?
If you can prove a formula A in a theory T containing elementary
arithmetic, then you can also prove Prov_T("A") in T, and hence
A<=>T("A"). This is very far from proving for every B, provable or not,
that B<=>Prov_T("B"). And again, the Gödel sentence for T does not say
"G has no proof" but "G has no formal proof in T", or rather is
equivalent, provably in T, to such a statement, i.e. T |- G <=>
~Prov_T("G"). If T is consistent, then it can't prove G, because if it
did, it would also prove Prov_T("G"). It also - usually - proves Cons_T
=> G, which only shows that Cons_T is not provable in T. If we happen to
know that Cons_T, then we have a proof of G, but since Cons_T is not
provable in T, we can't transform this into a formal proof of G in T.
If T did prove for every B that B<=>Prov_T("B"), it would prove that
0=1<=>Prov_T("0=1") and hence ~0=1<=>~Prov_T("0=1"). But since T proves
~0=1, it would also then prove ~Prov_T("0=1"), which amounts to
consistency of T. But since Gödel's proof, which can be carried out in
T, gives us Cons_T => G, we could use modus ponens to conclude G in T,
and since we have already established that T |/- G if T is consistent, T
would be contradictory. Therefore no consistent theory proves for every
formula B that B <=> Prov_T("B").
you haven't proven G if this formula is allowed.
g <-> proof(g)
Its a valid formula, if its presence refutes G then G hardly disproves it does it?
Herc
"Aatu Koskensilta" <aatu.kos...@xortec.fi> wrote in
> nope. reword the godel statement slightly...
> "this statement G is not provable in any system" and your formal proof
> of G is invalid.
You're speaking non-sense. That's like saying the four-colour theorem is
not true because if you change four to three it's false. Anyways, your
new G is simply false, and provably so in sufficiently strong theories.
> Its a valid formula, if its presence refutes G then G hardly disproves it does it?
For all formulae A, A<=>Prov_T("A") is indeed a perfectly well-formed
formula. It just happens it's not provable in T unless A is. In
particular, since T |- G<=>~Prov_T("G") (for the Gödel sentence of T,
which can be proved to exist), T can't prove G<=>Prov_T("G") provided
it's consistent.
>Ah so you are saying that the {Halting Problem} was NOT formed
>to produce a contradiction?
>
>if (Halts(Program))
> while(true); // loop forever
Peter, the way (or a way) to prove that something is *not* possible
is to show that it leads to a logical contradiction.
>Think about this for a few hundred more hours, and then get back to me.
>The ONLY reason that the {Halting Problem} is unsolvable is because
>it was specifically defined to be unsolvable.
No, it was *proved* to be impossible.
>It was made unsolvable by (in a sense) being forced to produce a >contradiction.
If I show that assuming A leads to a contradiction, then I have
proved that A is false. A in this case is "There exists a computer
program that solves the halting problem".
But then the Halting Problem is of no consequence because it is unsolvable
in the same way as these next three unsolvable problems:
(1) What times is it, yes or no?
(2) How far is it from Omaha to Chicago, red or blue?
(3) What are the colors on the flag of the United States of America, in
dollars and cents?
> > It was made unsolvable by
> > (in a sense) being forced to produce a contradiction.
>
> Assuming that the halting problem is solvable leads to a contradiction,
yes.
That's not quest what I was saying. The Halting Problem is
constructed from a contradiction:
if (Halts(Program))
while(true); // loop forever
forms a contradiction.
G is false? then there is no proof for G anywhere at all, G being
"this statement G is not provable in any system"
how do you put it....Since G is equivalent to its own
unprovability, we see that G is actually true
>
> > Its a valid formula, if its presence refutes G then G hardly disproves it does it?
>
> For all formulae A, A<=>Prov_T("A") is indeed a perfectly well-formed
> formula. It just happens it's not provable in T unless A is. In
> particular, since T |- G<=>~Prov_T("G") (for the Gödel sentence of T,
> which can be proved to exist), T can't prove G<=>Prov_T("G") provided
> it's consistent.
I'm not trying to prove G<->proof(G)
although I think its more evident than crators on the moon.
The English term mutually exclusive isn't getting through to you.
Call Forall x, x<->proof(x) F
Call ~proof(G) G
you're claiming G -> ~F
you ignore that F -> inconsistent(G)
effectively F -> ~G.
F XOR G take your pick
Herc
Which shows that the answer to the question is "no",
not that the question is invalid or ill-formed.
************************
David C. Ullrich
> "Aatu Koskensilta" <aatu.kos...@xortec.fi> wrote
>
> G is false? then there is no proof for G anywhere at all, G being
> "this statement G is not provable in any system"
But there are systems that prove false things. For example the theory T
with G as its only axiom.
I'll be off to home now.
>Call Forall x, x<->proof(x) F
>Call ~proof(G) G
>
>you're claiming G -> ~F
>you ignore that F -> inconsistent(G)
>
>effectively F -> ~G.
That's right. F -> ~G. So, if F is true,
then G is false. But look at what ~G says:
Since G <-> G is not provable, then
~G <-> G is provable.
So we have:
F -> G is false
F -> G is provable
So, if F is true, then G is false and G is *also* provable.
So, we have:
F -> some false statement is provable
Turning that around
If no false statement is provable, then F is false.
>
> If (DoesTheProgramHalt == true) return 1;
> else if (DoesTheProgramHalt == false) return 0;
> else return -1 // The Program NeitherHaltsNoDoesNotHalt
>
...what does the following program do (if supplied as it's own input):
If (DoesTheProgramHalt(input,input) == true) loop;
else if (DoesTheProgramHalt(input,input) == false) stop;
else stop;
Note that there are only 2 possible cases: either it loops or it stops
(halts). This means that DoesTheProgramHalt() m u s t return either true
or false if it correctly determines the behavior of its input(program).
Now if it returns false then ... and if it returns true then ...
F.
>>>If the input data is an English poem, (or any other invalid input) the
>>>Halt() function returns that it neither halts, nor does not halt.
>>
>>Since a TM is normally defined to read a very restricted set of input
>>(blank/not-blank), it will interpret the English poem the same as the
>>unary string that is equivalent to it.
>
>
> The point of the Turing Machine is that anything computable can be
> represented by it. Also Blank/Not Blank would be binary, and not
> unary.
>
>
Unary: 1111111 = 7
blank = end of input.
--
Will Twentyman
email: wtwentyman at copper dot net
no, you missed the "effectively", go back a step and the XOR is reasoning
about the acceptance of the formula into the model, not their boolean values
in the model. this is (intended as) a meta analysis of the formula's inclusion,
not a semantic analysis of their values.
If F is an axiom/formula, then G makes the model inconsistent.
If G is a formula, then F makes the model inconsistent.
Why do you chose one over the other?
You seem to have favored G here because ~G leads to a contradiction,
G has no solution as false so it has a built in solution as true.
F is just an ordinary formula, either true or false.
G does not disprove F, they are mutually exclusive.
Aatu claimed :
and since we have already established that T |/- G if T is consistent, T
would be contradictory. Therefore no consistent theory proves for every
formula B that B <=> Prov_T("B").
He only showed G in T is consistent without the axiom F<->proof(F).
This is your reasoning :
ForAll n e N, 1/n is definable.
Therefore ForAll numbers r, 1/r is definable.
Therefore 0 is not an allowed number.
There is nothing inconsistent with that reasoning, but you seem to have adopted
"consistent" as "correct".
Herc
Its just as valid as the question:
What times is it yes or no?
(In other words its an absurd question)
[stuff deleted]
>> So we have:
>>
>> F -> G is false
>> F -> G is provable
>>
>> So, if F is true, then G is false and G is *also* provable.
>> So, we have:
>>
>> F -> some false statement is provable
>>
>> Turning that around
>>
>> If no false statement is provable, then F is false.
[more stuff deleted]
>If F is an axiom/formula, then G makes the model inconsistent.
Right. But luckily, F is not an axiom.
>If G is a formula, then F makes the model inconsistent.
But G certainly *is* a formula. Godel explicitly showed
how to construct the formula G.
>Why do you chose one over the other?
Because F is not a formula (in the language of PA), but G
is. Your definition of F is
Forall x, x<->proof(x)
which involves quantification over sentences (or propositions).
That is not possible in first-order logic. (If you want to go to
second-order logic, I'm not sure that Godel's theorem applies
directly).
In contrast, G is a simple quantification over natural numbers.
In some formulations of Godel's theorem (MRDP version) G has
the form of a claim that a specific polynomial equation has no
integer solutions. (Exactly which polynomial equation is a little
complicated). However, G is constructed so that it is provable
(in the metatheory) that G is true (as a statement of arithmetic)
if and only if G is not provable from the axioms of PA.
>You seem to have favored G here because ~G leads to a contradiction,
>G has no solution as false so it has a built in solution as true.
>F is just an ordinary formula, either true or false.
No, F is not an ordinary formula. In an ordinary formula of
arithmetic, you can only quantify over natural numbers. So
a statement such as
Forall x, x<->proof(x)
is syntactically incorrect. x is a number, not a sentence,
so it makes no sense to say x <-> proof(x). Only a sentence
can be on the left-hand side of <->.
Very dubious IMO since every formula is represented by a number.
Consider the following predicate:
Proof(x,y,z)
having the following interpretation: "x is the godel number of a proof X of a formula Y
(one with one free variable and godel number y) which has the integer z substituted into it".
The "proof X" referred to here may itself be considered a formula for the purpose of having a
Godel number assigned to it.
Note that the basic symbols to which code numbers were attached did not
include the predicate symbol "Proof" or any other predicate symbol except
equality (=). Indeed, "Proof(x,y,z)" is just our own shorthand for an
immensely long expression with three free variables x, y, and z - or in Godel's
notation, x1, x11, and x111. This expression includes a number of procedures,
including the following:
1. given an integer, produce the string of which integer it is the Godel number.
2. given a string, check whether it is a formula
3. given a sequence of formulas, check whether it is a proof for the last
formula in the sequence.
All these procedures are computable. Suppose that the formula Y is fed its own
godel number and that we deny the existence of a proof within the formal system
of the resulting formula:
~ExProof(x,y,y)
In words, the formula Proof(x,y,y) says, "x is the Godel number of a proof of
the formula obtained by substituting its own Godel number y for its one free
variable". Consequently, to write ~Ex in front of this is to deny the existence
of such a proof.
Now any such predicate expressible in the formal system has a godel number,
call the godel statement g.
Suppose ~ExProof(x,g,g) is provable, let p be the godel number of its proof.
Then Proof(p,g,g) is true since p is proof of g, but Proof(p,g,g) contradicts
~ExProof(x,g,g) so no proof p exists.
The formula ~ExProof(x,g,g) is certainly true because we have just established
the claim it makes about itself - that it has no proof.
Straight from the textbook, using quantification over Proof (the godel numbers).
> >F is just an ordinary formula, either true or false.
>
> No, F is not an ordinary formula. In an ordinary formula of
> arithmetic, you can only quantify over natural numbers. So
> a statement such as
>
> Forall x, x<->proof(x)
>
> is syntactically incorrect. x is a number, not a sentence,
> so it makes no sense to say x <-> proof(x)
So do you retract this assertion?
Herc
The halting problem is "Does TM M halt on input x?" How is this question
even superficially similar (syntactically) to any of the questions above?
groente
-- Sander
>
>"David C. Ullrich" <ull...@math.okstate.edu> wrote in message
>news:96dbc0h5k8qc9jjoq...@4ax.com...
>> On Tue, 08 Jun 2004 12:24:30 GMT, "Peter Olcott"
>> <olc...@worldnet.att.net> wrote:
>>
>> >> Exactly what _is_ invalid about "Does there exist a Turing
>> >> machine which will determine whether or not another Turing
>> >> machine halts with a certain input?"
>> >
>> >if (Halts(Program))
>> > while(true); // loop forever
>> >
>> >forms a contradiction.
>>
>> Which shows that the answer to the question is "no",
>> not that the question is invalid or ill-formed.
>
>Its just as valid as the question:
>
>What times is it yes or no?
>(In other words its an absurd question)
Only in your imagination.
(Before you complain that that's not much of a refutation
of your argument please note that you haven't _given_ an
argument, just an unsupported assertion. Since nobody else
on the planet agrees you might want to try to explain
just what's absurd about the question...)
************************
David C. Ullrich
Its not syntactically similar its semantically analogous. The {Halting
Problem}
merely forms and absurd question, just as the above three questions are
absurd.
Finally you have admitted that you are a nutcase. Good work |-|erc. You are
on the road to recovery.
L
if (Halts(Program))
while(true); // loop forever
You are asking the Halt function to do what is analytically
impossible. (impossible by definition) Its like asking a cad
program to draw a square circle. Further still saying that
failure to solve the Halting Problem will forever place any
sort of real limit on the future of computer science is like
saying that CAD programs will never be complete because
they will never be able to draw square circles.
Why is it an absurd question? Do you not understand it? Say, you just
started the TM on input x, and after a number of steps it halted. What
would your answer to the question "Does TM M on input x" be?
groente
-- Sander
> Peter [Troll] Olcott wrote:
>>>>
>>>> (1) What times is it, yes or no?
>>>> (2) How far is it from Omaha to Chicago, red or blue?
>>>> (3) What are the colors on the flag of the United States of America, in
>>>> dollars and cents?
>>>
>>> The halting problem is "Does TM M halt on input x?" How is this question
>>> even superficially similar (syntactically) to any of the questions above?
>>>
>> It's not syntactically similar its semantically analogous. The {Halting
>> Problem} merely forms and absurd question, just as the above three
>> questions are absurd.
>>
> Why is it an absurd question? Do you not understand it? Say, you just
> started the TM on input x, and after a number of steps it halted. What
> would your answer to the question "Does TM M [halt] on input x" be?
>
He will answer:
"This is an absurd question!"
qed. Case closed.
F.
>> (Before you complain that that's not much of a refutation
>> of your argument please note that you haven't _given_ an
>> argument, just an unsupported assertion. Since nobody else
>> on the planet agrees you might want to try to explain
>> just what's absurd about the question...)
>
>if (Halts(Program))
> while(true); // loop forever
>
>You are asking the Halt function to do what is analytically
>impossible.
Huh? I didn't ask anything about those two lines of
pseudo-code. I asked exactly what _is_ invalid about
(*) "Does there exist a Turing machine which will determine
whether or not another Turing machine halts with a
certain input?"
So far all you've done is (sort of) explain why the
answer to (*) is "no". That's not what I asked.
>(impossible by definition) Its like asking a cad
>program to draw a square circle. Further still saying that
>failure to solve the Halting Problem will forever place any
>sort of real limit on the future of computer science is like
>saying that CAD programs will never be complete because
>they will never be able to draw square circles.
>
************************
David C. Ullrich
>
> The halting problem is "Does TM M halt on input x?" How is this question
> even superficially similar (syntactically) to any of the questions above?
>
Peter is mixing up several things. :-(
First, it's a simple fact that a TM will either hold on input x, or
loop. There is simply no other possibility. (Which one?)
Now the question (Halting problem) actually is not "Does TM M halt on
input x?" but is there a TM (program) which can _decide_ (evaluate) IF
any TM with a given input may halt or not.
The difference is the following, the answer to the question:
"Does TM M halt on input x?"
depends on "context" and "knowledge": If you ask a certain person who
just knows the states of the TM in question and input x several answer
would be possible:
Yes.
No.
I don't know.
Here Peter is right, b u t the original Halting Problem asks for a
"procedure" which is able to give the answers yes or no! I.e. which is
able do determine i f any given TM with a given input will halt or not.
(Since there is no "third case" for a TM, the problem is well defined.)
And the answer is: No, there is no such TM (program, procedure).
F.
P.S.
I hope I got it right. ;-)
>> >> |-|erc says...
>> >>
>> >> >Call Forall x, x<->proof(x) F
>> >> >Call ~proof(G) G
[stuff deleted]
>> Because F is not a formula (in the language of PA), but G
>> is. Your definition of F is
>>
>> Forall x, x<->proof(x)
>>
>> which involves quantification over sentences (or propositions).
>> That is not possible in first-order logic. (If you want to go to
>> second-order logic, I'm not sure that Godel's theorem applies
>> directly).
[stuff deleted]
>Very dubious IMO since every formula is represented by a number.
In the expression
Forall x, x<->proof(x)
it is perfectly fine for x to be a number (a code for a
formula) in the expression proof(x). But, as I said, it
is not perfectly fine to use a number on the left side of
x <-> proof(x)
That's just syntactically incorrect, because x is not
a formula.
You could make it syntactically correct by introducing
a truth predicate True(x) with the interpretation that
True(x) holds if and only if x is a number coding a true
sentence. But there *is* no truth predicate for arithmetic,
and if you introduce one by axiom, the resulting system is
inconsistent, as proved by Tarski.
[stuff deleted]
>> No, F is not an ordinary formula. In an ordinary formula of
>> arithmetic, you can only quantify over natural numbers. So
>> a statement such as
>>
>> Forall x, x<->proof(x)
>>
>> is syntactically incorrect. x is a number, not a sentence,
>> so it makes no sense to say x <-> proof(x)
>
>So do you retract this assertion?
No, what I said was perfectly correct.
>Its [the unsolvability of the halting problem]
> just as valid as the question:
>
>What times is it yes or no?
>(In other words its an absurd question)
No, it's not. Let's go through the proof again, and you
can see that there is nothing incorrectly formed about it.
For simplicity, let me use strings rather than naturals as
the basic data type, since it is more obvious how to code
a program as a string than as a number (the code is just
the source code for the program).
In the following, the word "halt" should be interpreted
as running to completion. Shutting off the power to a
computer does not imply that the program running on it
has halted.
1. Definition: If P is a program that takes an argument of
type string, and p is the source code for P, then we say
that P is "non-self-halting" if the computation P(p) runs
forever.
2. Definition: If S is a set of strings, and P is any program
that takes a single argument of type string, then we say that
P is a "recognizer" for set S if for any string s
P(s) halts
<->
s is in the set S
For example, the program that looks at the first character of
a string and halts if that character is '0' and otherwise enters
an infinite loop is a recognizer for the set of all strings starting
with a '0'.
Let NSH be the set of all strings s that are codes for
non-self-halting programs. More formally, if P is any
program, and p is its source code, then
p in NSH <-> P(p) never halts
3. Definition: If S is a set of strings, and P is a program
that takes a single argument of type string, and s is any string,
then we say that s is a S-failure for P if one of the following
occurs
a. s is in S, but P(s) doesn't halt.
b. s is not in S, but P(s) halts.
By definition of "recognizer", if s is a S-failure for P, then
P is not a recognizer for S.
4. Theorem: Let P be any program that takes one string as an
input. Let p be its code. Then p is a NSH-failure for P.
Proof: Just apply the definitions:
p is in NSH <-> P(p) never halts, by definition of NSH.
Therefore, either p is in NSH and P(p) never halts, or
p is not in NSH and P(p) halts.
Therefore, p is a NSH-failure for P, by definition.
5. Corollary: There is no recognizer for the set NSH.
>if (Halts(Program))
> while(true); // loop forever
>
>You are asking the Halt function to do what is analytically
>impossible.
Right.
Halt cannot possibly give the correct answer in this case.
You agree with that. Well, that's what the unsolvability
of the halting problem says: that it is analytically impossible
for there to be a program Halt that always gives the correct
answer to the question "Does program P halt?" that works for
every program P.
The logical structure is this:
1. Assume that there is a program Halt which takes
a program as an argument and attempts to return "true"
if the program halts, and "false" if it doesn't halt.
2. Construct a program P such that it is analytically
impossible for Halt to give the correct answer to Halt(P).
3. Conclude that Halt cannot possibly give the correct
answer in all cases. That is, Halt does not solve the
halting problem in all cases.
>> Its not syntactically similar its semantically analogous. The {Halting
>> Problem} merely forms an absurd question, just as the above three
>> questions are absurd.
>
>Why is it an absurd question?
Here's my psychological analysis of why Peter thinks
it is absurd.
What Peter is doing is "anthropomorphising" the Halting program. He's
putting himself in the position of Halt, and he's imagining that Halt
is asked his opinion on whether this or that program halts. Then the
particular program that Halt is asked to pass judgement on is felt
by Peter to be an "unfair question". There is no way for Halt
to answer the question---it isn't a matter of lack of intelligence,
it is that answering the question correctly is analytically impossible.
So Peter thinks that this is an unfair thing to hold against our poor
Halt program.
It's exactly as if Peter himself were being asked a series of yes-no
questions, and he is punished if he answers a question incorrectly.
Then questioner's first question is:
Will your answer to my first question be "no"?
Peter cannot possibly answer that question correctly, but it's
not because Peter is stupid, or because he lacks some key piece
of knowledge. It doesn't matter *how* smart Peter is, he can
never answer that question correctly.
So, I think that Peter's objection to impossibility proofs
(including Godel's theorem and Turing's proof of the unsolvability
of the halting problem) is that they don't intuitively demonstrate
a limitation on the *intelligence* or *power* of the systems
(Peano Arithmetic in the one case or the Halt program in the other
case) to say that they can't correctly answer a particular question.
So Peter thinks these proofs are somehow unfair.
But the bottom line, of course, is that it doesn't matter whether
the questions are unfair or not, it is provable that there are
well-defined questions that Peano Arithmetic or a purported Halt
program cannot answer correctly.
Not really.
>
>
>>
>> Also, TM's don't crash. :-)
>
> do so.
A TM may perform unexpectedly because of a specification error
or unexpected input, but not crash. A TM is too simple a
beast to crash, really.
>
>>
>> No, it does not disprove such a program. A fixed-cycle halter
>> is easy to write -- just run the simulated TM for that number
>> of cycles.
>
> not the program I was talking about, can you solve an
> exponential program in polynomial time. i.e. is there
> a haltexp that halts in polynomial time (a fixed
> cycle halter using a simple type of emulator wont work).
Why not?
>
> Herc
>
--
#191, ewi...@earthlink.net
It's still legal to go .sigless.
This is the absurd part
if (Halts(ThisProgram))
while(true); // loop forever
False dilemma again.
A correct answer to the above question would be:
The answer to your question is negatively affirmed.
There are hundreds and hundreds of such correct answers.
Yet whenever one restricts the possible answers to Yes / No this
leaves countless questions that can not possibly be correctly
answered. Also when one asks a question and restricts the answer
to Yes / No, and the answer does not fit within this restrictive dichotomy,
it is the one asking that has failed, not the one responding, or failing
to respond.
> able do determine if any given TM with a given input will halt or not.
Actually the only correct answer to this question would be
of the form that this question itself is flawed.
rubbish,
1/ you snipped off the LHS of the formula
2/ you're just quoting "this is right"
3/ your complaint that formula cannot be quantified is the issue which you snipped
Herc
an effective halting program is not useful?
>
> >
> >
> >>
> >> Also, TM's don't crash. :-)
> >
> > do so.
>
> A TM may perform unexpectedly because of a specification error
> or unexpected input, but not crash. A TM is too simple a
> beast to crash, really.
it can compute anything and its simple?
> >
> >>
> >> No, it does not disprove such a program. A fixed-cycle halter
> >> is easy to write -- just run the simulated TM for that number
> >> of cycles.
> >
> > not the program I was talking about, can you solve an
> > exponential program in polynomial time. i.e. is there
> > a haltexp that halts in polynomial time (a fixed
> > cycle halter using a simple type of emulator wont work).
>
> Why not?
because you can't work out any maths proofs for yourself and this one
isn't in the book.
Herc
recovery is a word you'll be hearing a lot of
Herc
Daryl is showing his true colors here, the objection is about the
wrongness of the construction >>>do an infinite loop<<<
this is quite clear, yet Daryl just twists his words into, YOU AGREE
HALT IS IMPOSSIBLE. There is no binding to variables in Peters
argument that shows any of what Daryl is responding about, just
a cheap shot by Daryl to *ignore* any points of his possible flaw.
See if we can construct a halting proof without the infinite loop.
Program Test (f, a)
if Halt(f, a) = 1 then //halts
value = UTM(f, a) + 1
else
value = 0
Is this program OK Peter, UTM is just an emulator that calculates F(a).
Herc
No, I said they were yes-no questions. Anything other than
"yes" or "no" is considered incorrect. I'm the one who's
making up the game, and I get to say what the
rules are. The rules are: you must answer each yes-no
question with "yes" or "no". If your answer is incorrect,
you are punished.
>Yet whenever one restricts the possible answers to Yes / No this
>leaves countless questions that can not possibly be correctly
>answered.
Then don't answer anything in those cases.
But if the question is
Will Peter answer "no" to this question?
then the question actually *is* a yes/no question, although
you cannot answer it correctly.
>Also when one asks a question and restricts the answer
>to Yes / No, and the answer does not fit within this restrictive dichotomy,
>it is the one asking that has failed, not the one responding,
>or failing to respond.
You seem to be worried about whose *fault* it is. It's not a matter
of placing blame---it's just noting that there is a legitimate yes/no
question that you cannot answer correctly.
It's just a fact about computer programs that no computer program
can always give the correct answer to the question "Does program P
halt?".
No, that's an incorrect answer. If you have a program P, and
you ask "Does P ever halt?" then that's a perfectly valid
question. There is nothing flawed about the question. The
fact that P was created specifically as to thwart the Halt
doesn't make any difference. P is a perfectly legal program,
and it is a perfectly valid question to ask whether it halts.
What's wrong about it? An infinite loop is a perfectly good
program. It's a "while" loop in which the condition is always
true. For instance:
int i = 1;
while (i == i) {
i = i+1;
>rubbish,
>1/ you snipped off the LHS of the formula
I have no idea what you are talking about. The question is whether
forall x, x <-> proof(x)
is a definable formula of PA. It isn't. Your post
quoted a textbook that was discussing a *different*
formula, namely the Godel sentence.
>2/ you're just quoting "this is right"
I gave you the reasons for saying it.
>3/ your complaint that formula cannot be quantified is the issue
>which you snipped
I don't know what you are talking about. I snipped a long
quotation of yours from a textbook because it appeared irrelevant
to me. Here's what I snipped: (Below the dashed line). Nowhere
does it give any meaning to the formula
forall x, x <-> Proof(x)
--
Daryl McCullough
Ithaca, NY
---------------------------------
Consider the following predicate:
Proof(x,y,z)
having the following interpretation: "x is the godel number of a proof X of a
formula Y
(one with one free variable and godel number y) which has the integer z
substituted into it".
The "proof X" referred to here may itself be considered a formula for the
purpose of having a
Godel number assigned to it.
Note that the basic symbols to which code numbers were attached did not
include the predicate symbol "Proof" or any other predicate symbol except
equality (=). Indeed, "Proof(x,y,z)" is just our own shorthand for an
immensely long expression with three free variables x, y, and z - or in Godel's
notation, x1, x11, and x111. This expression includes a number of procedures,
including the following:
1. given an integer, produce the string of which integer it is the Godel number.
2. given a string, check whether it is a formula
3. given a sequence of formulas, check whether it is a proof for the last
formula in the sequence.
All these procedures are computable. Suppose that the formula Y is fed its own
godel number and that we deny the existence of a proof within the formal system
of the resulting formula:
~ExProof(x,y,y)
In words, the formula Proof(x,y,y) says, "x is the Godel number of a proof of
the formula obtained by substituting its own Godel number y for its one free
variable". Consequently, to write ~Ex in front of this is to deny the existence
of such a proof.
Now any such predicate expressible in the formal system has a godel number,
call the godel statement g.
Suppose ~ExProof(x,g,g) is provable, let p be the godel number of its proof.
Then Proof(p,g,g) is true since p is proof of g, but Proof(p,g,g) contradicts
~ExProof(x,g,g) so no proof p exists.
The formula ~ExProof(x,g,g) is certainly true because we have just established
the claim it makes about itself - that it has no proof.
--------------------------------
Regarding
Your definition of F is
Forall x, x<->proof(x)
which involves quantification over sentences (or propositions).
That is not possible in first-order logic
Are you saying this is not possible also then?
> ~ExProof(x,y,y)
Herc
It's not all that effective. At best, it computes whether
a function can halt in N cycles in the same time one can
run the function using N cycles. At worst, it requires
an emulator.
Unless I'm missing something (which is admittedly possible).
>
>
>>
>> >
>> >
>> >>
>> >> Also, TM's don't crash. :-)
>> >
>> > do so.
>>
>> A TM may perform unexpectedly because of a specification error
>> or unexpected input, but not crash. A TM is too simple a
>> beast to crash, really.
>
>
> it can compute anything and its simple?
It cannot compute everything. Of course, one might make the case
that that which cannot be computed may not be that interesting.
>
>
>> >
>> >>
>> >> No, it does not disprove such a program. A fixed-cycle halter
>> >> is easy to write -- just run the simulated TM for that number
>> >> of cycles.
>> >
>> > not the program I was talking about, can you solve an
>> > exponential program in polynomial time. i.e. is there
>> > a haltexp that halts in polynomial time (a fixed
>> > cycle halter using a simple type of emulator wont work).
>>
>> Why not?
>
>
> because you can't work out any maths proofs for yourself and this one
> isn't in the book.
Ah, so you're suggesting I'm part of the Godel/Turing/Cantorian
Conspiracy To Suppress The Proof That All Sets Are Closed And
All Reals Are Countable?
Woo.
(Hmm.... GTCCTSTPTASACAARAC. Perhaps a better name would be
"The Unpronounceable Acronym Conspiracy"...)
Of course, I can't seem to work out *your* math proofs. But mine
seem to work fine, although I can't claim originality.
But then, this is well-trodden territory. Still, let's start with
the simple stuff.
Define "equals".
I'll make it even simpler: assume two real numbers r and s have
Cauchy sequences r_i and s_i. Then r and s are equal iff
the sequence t_i = r_i - s_i has limit 0.
If you really want I'll use Dedekind cuts instead... :-)
The two definitions are equivalent anyway.
I've already stipulated that the naive Q -> R mapping will result
in a gray line -- although "gray" in this context would be
almost white, as the Lebesgue measure of Q intersect [0,1] is 0,
whereas the Lebesgue measure of R intersect [0,1] is 1.
If one colors the former black and the latter white, the line
is white for all intents and purposes, even though Q is dense.
But I can't say it is white, just almost white, as there
are bits of black (actually, infinite pinpricks) -- 1/2,
2/3, 1/3, and such, for instance. But there's also pi/4,
which is not rational by any stretch of the imagination
(even though it's approximatable by at least one strictly
monotonic rational Cauchy sequence) and is therefore white.
If one picks a number in [0,1], the probability that it
is in a set S which is a subset of [0,1] turns out to be
merely the Lebesgue measure of S. Since (R - Q) intersect
[0,1] has measure 1 it is virtually certain the number
I pick is irrational -- in fact, it's virtually certain
it's transcendental as well. (I'll bore you with details
of a possible mapping of N to A if you want; suffice it
to say for now that said mapping can be done.)
Or one can look at it this way. If numbers r and s are equal,
then their digit expansions match for any finite n. If I am
given two numbers t and u, then I can prove them unequal if I
can find a d such that t(d) and u(d) differ, and, as a Pedant
Point, t(d+1) and u(d+1) are not 0 and 9, or 9 and 0. (This
sidesteps the old 0.999... = 1.000 problem, of course.) This
despite the fact that floor(t * 10^n) / 10^n is rational for
any nonnegative integer n and any t in the interval [0,1].
Therefore the diagonal construction works, if done carefully enough
to avoid the infinite 9-0 problem -- even though every prefix
of the diagonal number be in the list -- not unreasonable since
the list is supposed to contain all reals.
Or one can do it this way. Assume for the nonce that the sequence
S = {0.3, 0.33, 0.333, ... } is also a set. This set has a lower
bound (0.3). Does it have an upper bound? The sequence is
strictly monotonically increasing; therefore, for every s_n,
s_{n+1} > s_n and therefore there is no upper bound, although
there is a supremum, namely, 1/3. But 1/3 is not in the set,
since s_n = (10^n - 1) / (3 * 10^n) != 1/3 for any integer n.
(Infinity is not an integer. It's not a real number either.)
I'm not sure this argument is even all that recognizable
as a horse anymore. Between my cudgel, Barbara's shillelagh,
and other's clubs it's been liquefied.
Of course, from an effectively computable standpoint,
all numbers are finite and rational. The approximation
commonly used, for instance, has to be a multiple of a
power of 2; furthermore, the multiplier cannot exceed
2^52, and the multiplicand must be between the range
2^-1076 and 2^+972 (I might be off by a bit or two).
Also, if one adds or subtracts two numbers, the result
may be rounded to be in this form under certain conditions,
and some of the bit representations are sacrificed and
treated as though they are either 0, +oo, -oo, or
some undefined value with well-defined properties
(e.g. 0 * NaN = NaN, NaN + 1 = NaN).
Infinite decimal expansions are impossible to write out in full,
although an interesting computational method is applicable
to pi, if one wants an arbitrary hex digit. See Equation
29 in
http://mathworld.wolfram.com/PiFormulas.html
for example.
>Sander Bruggink wrote:
>>Why is it an absurd question? Do you not understand it? Say, you just
>>started the TM on input x, and after a number of steps it halted. What
>>would your answer to the question "Does TM M halt in input x" be?
[Forgotten "halt" in the above quote fixed.]
> This is the absurd part
>
> if (Halts(ThisProgram))
> while(true); // loop forever
No, this is not a part of the halting problem. It is a part of the
*proof* that the halting problem is unsolvable.
Please tell what part of the halting problem ("Does TM M halt on input
x") is incorrectly stated. We all know already that assuming that it can
be solved yields an absurdity.
groente
-- Sander
>Regarding
>
> Your definition of F is
>
> Forall x, x<->proof(x)
>
> which involves quantification over sentences (or propositions).
> That is not possible in first-order logic
>
>
>Are you saying this is not possible also then?
>> ~ExProof(x,y,y)
No, in Proof(x,y,y), x and y are *numbers*, not sentences.
(They are numbers that *code* for sentences, but they are
still numbers.)
Proof(x,y,y) is a formula involving x and y. This is in contrast to the
expression
For all x, x <-> Proof(x)
In that expression, if you meant for x to be a *number*
then the left-side of the <-> is incorrect --- only formulas
can appear on the left side of <->. If you meant for x
to be a sentence, then the quantifier Forall x makes no
sense, because you can only quantify over numbers.
Come get some boy
|_
Here is the Halting Problem:
(4) Does there exist a Turing Machine that when given as inputs a Turing
Machine M and an input string x will answer "yes" if M halts on x and will
answer "no" if M does not halt on x?
This does not contain a flaw analogous to those in (1), (2), and (3) above.
The question has the form: "Does there exist a certain object?" It is similar
to
(5) Does there exist a largest prime number?
(6) Does there exist a pair of integers c and d such that e + pi = c/d?
There is no clause in (4) that restricts the type of answer you may give.
You are not being told to answer "red or blue" or in "dollars and cents."
You are not even being told to answer "yes or no." You can answer
"I don't know" for all I care. But there is an unrefuted mathematical proof
that the answer to (4) is "no." Forget about the phrase "the unsolvability of
the halting problem." Think of it this way: "the answer to (4) above is 'no'."
Again, no one is restricting your type of answer. Although, I would give you
a quizzical look if you answered "blue" to (4).
-Leonard
>
> > > It was made unsolvable by
> > > (in a sense) being forced to produce a contradiction.
> >
> > Assuming that the halting problem is solvable leads to a contradiction,
> yes.
>
> That's not quest what I was saying. The Halting Problem is
> constructed from a contradiction:
>Here is the Halting Problem:
>
>(4) Does there exist a Turing Machine that when given as inputs a Turing
>Machine M and an input string x will answer "yes" if M halts on x and will
>answer "no" if M does not halt on x?
The following is a nitpick, but Peter latches onto any conceivable
triviality if it helps him avoid the content of what you are saying.
A Turing machine cannot take another Turing machine as an argument,
it can only take a *string* as an argument. So the halting problem
has to be phrased as
(4) Does there exist a Turing Machine that when given as inputs a
string that is a code for a Turing Machine M and an input string
x will answer "yes" if M halts on x and will answer "no" if M does
not halt on x?
But this correction also has a problem, because some strings might
not code for any Turing Machine at all.
The way around this is one of the following:
1. Pick a coding of Turing Machines as strings that is *total*. That is,
every string should code for some Turing Machine, even a string such as
the text of Romeo and Juliet.
2. Make up some default behavior if the input doesn't code for a Turing
Machine. So you could say:
Does there exist a Turing Machine that when given as inputs two
strings m and x, will output "yes" if m codes for a Turing Machine
M which halts on input x, and will output "no" otherwise.
So with this formulation, if you hand the Turing Machine nonsense, it
should output "no".
Okay fine, then the Halting Problem is solvable because the proof is flawed.
I no longer agree that this is a fact, because (apparently) the absurd
part of the problem exists in the proof itself. A computer program
can correctly determine whether or not any other correct computer
program will halt. The counter-example provided to dispute this claim
is an ill-formed program, and thus no more valid that if an English Poem
were submitted to see if the English Poem would halt.
> There is no clause in (4) that restricts the type of answer you may give.
> You are not even being told to answer "yes or no."
Restricting the answer to Yes or No is entailed by the semantics of the
question. An answer of "blue" to this question would be incorrect
because it is neither "yes" nor "no".
Or here is a totally other way of looking at it.
The answer is YES, because the counter-example program
neither halts, nor does not halt, thus escapes the question by
a loophole.
What are the colors of the flag of the United States of America
in dollars and cents? would then be a perfectly valid question.
All questions that are defined to be impossible are valid questions.
Just because a question is specifically designed to be impossible
to answer does not in any way refute the legitimacy of the question.
(This is where your line-of-reasoning leads)...
This is not an example of a valid infinite loop.
An example of a valid (useful) infinite loop is
the wait for user input loop. Until you tell the
program to end, it continues.
is the intended formula possible? and don't rely on the truth of Godel
statements to deny it.
Herc