The halting problem being undecidable is NOT a fucking axiom; you
can't go about saying:

"Since the halting problem is known to be undecidable blah blah fucking
blah" in your fucking proofs.

Mr Flibble is very cross at all the laziness in this area of "research".

/Flibble

On 7/16/2021 4:33 PM, Mr Flibble wrote:
> The halting problem being undecidable is NOT a fucking axiom; you
> can't go about saying:
>
> "Since the halting problem is known to be undecidable blah blah fucking
> blah" in your fucking proofs.
>
> Mr Flibble is very cross at all the laziness in this area of "research".
>
> /Flibble
>

It is considered to be a theorem, thus considered to be equivalent to an
axiom.

People are so stupid that all of academia still thinks that the Liar
Paradox is a very difficult puzzle rather than simply an expression of
language that is not a truth bearer because it is erroneous.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

Mr Flibble <flibble@reddwarf.jmc> writes:

> The halting problem being undecidable is NOT a fucking axiom;

Agreed. It follows logically from most reasonable sets of axioms.

Interestingly, halting being decidable /can/ be taken as an axiom
without introducing any inconsistency.

> you can't go about saying:
>
> "Since the halting problem is known to be undecidable blah blah fucking
> blah" in your fucking proofs.

It's perfectly reasonable to state theorems as being known. We know
there is no largest prime. We know that a^2 + b^2 = c^2 for right
triangles...

--
Ben.

On 7/16/2021 4:21 PM, Ben Bacarisse wrote:
> Mr Flibble <flibble@reddwarf.jmc> writes:
>
>> The halting problem being undecidable is NOT a fucking axiom;
>
> Agreed. It follows logically from most reasonable sets of axioms.
>
> Interestingly, halting being decidable /can/ be taken as an axiom
> without introducing any inconsistency.
In what base system or systems is the above true? I'm thinking "in the
sense" that Godel follows in systems that allow sufficient arithmetic.
I'm not sure I'm asking this question in the best way; if not, please
help me out.
--
Jeff Barnett

Jeff Barnett <jbb@notatt.com> writes:

> On 7/16/2021 4:21 PM, Ben Bacarisse wrote:
>> Mr Flibble <flibble@reddwarf.jmc> writes:
>>
>>> The halting problem being undecidable is NOT a fucking axiom;
>> Agreed. It follows logically from most reasonable sets of axioms.
>> Interestingly, halting being decidable /can/ be taken as an axiom
>> without introducing any inconsistency.
>
> In what base system or systems is the above true? I'm thinking "in the
> sense" that Godel follows in systems that allow sufficient arithmetic.
> I'm not sure I'm asking this question in the best way; if not, please
> help me out.

And I'm sure I'm not putting correctly. What I mean is that the theory
of halting-oracle TMs is consistent. Of course, it has it's own halting
theorem: halting-oracle TM halting is not decidable by any
halting-oracle TM and there's an infinite chain of such theories.

--
Ben.

On 7/16/2021 5:11 PM, Ben Bacarisse wrote:
> Jeff Barnett <jbb@notatt.com> writes:
>
>> On 7/16/2021 4:21 PM, Ben Bacarisse wrote:
>>> Mr Flibble <flibble@reddwarf.jmc> writes:
>>>
>>>> The halting problem being undecidable is NOT a fucking axiom;
>>> Agreed. It follows logically from most reasonable sets of axioms.
>>> Interestingly, halting being decidable /can/ be taken as an axiom
>>> without introducing any inconsistency.
>>
>> In what base system or systems is the above true? I'm thinking "in the
>> sense" that Godel follows in systems that allow sufficient arithmetic.
>> I'm not sure I'm asking this question in the best way; if not, please
>> help me out.
>
> And I'm sure I'm not putting correctly. What I mean is that the theory
> of halting-oracle TMs is consistent. Of course, it has it's own halting
> theorem: halting-oracle TM halting is not decidable by any
> halting-oracle TM and there's an infinite chain of such theories.

I was aware the TM + ORACLE* hierarchy has no total halt deciders
deciders at the same level as the decidee. I was more curious about what
the axioms might contain to even be able to talk about mechanical
computations, deciders, and halting. It occurred to be that I had never
questioned what type of minimal axiomatic support one needs to work on
these topics.

I'm sure that embedding in ZF (or maybe even PA) is probably a good
start but what other than a few definitions must be added to do work in
this area. (I know that ZF and PA theorems can be expressed and proved
proved without definitions. However those definitions are usually made
for the edification of the reader so that we can check that "terms" are
represented similarly among the statements of multiple theorems.)

Thanks for responding.
--
Jeff Barnett

Mr Flibble <flibble@reddwarf.jmc> wrote:
> The halting problem being undecidable is NOT a fucking axiom;

No, it's not any other sort of axiom either. It's a theorem.

> you can't go about saying:

> "Since the halting problem is known to be undecidable blah blah fucking
> blah" in your fucking proofs.

You can, in any sort of proof, not just in fucking proofs. It's a
proven theorem.

> Mr Flibble is very cross at all the laziness in this area of "research".

I note how you put "research" into quote marks, and agree with that
totally. The question of the halting problem was completely settled in
the 20th century.

> /Flibble

--
Alan Mackenzie (Nuremberg, Germany).

On Sat, 17 Jul 2021 12:00:54 -0000 (UTC)
Alan Mackenzie <acm@muc.de> wrote:

> Mr Flibble <flibble@reddwarf.jmc> wrote:
> > The halting problem being undecidable is NOT a fucking axiom;
>
> No, it's not any other sort of axiom either. It's a theorem.
>
> > you can't go about saying:
>
> > "Since the halting problem is known to be undecidable blah blah
> > fucking blah" in your fucking proofs.
>
> You can, in any sort of proof, not just in fucking proofs. It's a
> proven theorem.

Prove it.

>
> > Mr Flibble is very cross at all the laziness in this area of
> > "research".
>
> I note how you put "research" into quote marks, and agree with that
> totally. The question of the halting problem was completely settled
> in the 20th century.

Prove it.

/Flibble

Mr Flibble <flibble@reddwarf.jmc> wrote:
> On Sat, 17 Jul 2021 12:00:54 -0000 (UTC)
> Alan Mackenzie <acm@muc.de> wrote:

>> Mr Flibble <flibble@reddwarf.jmc> wrote:
>> > The halting problem being undecidable is NOT a fucking axiom;

>> No, it's not any other sort of axiom either. It's a theorem.

>> > you can't go about saying:

>> > "Since the halting problem is known to be undecidable blah blah
>> > fucking blah" in your fucking proofs.

>> You can, in any sort of proof, not just in fucking proofs. It's a
>> proven theorem.

> Prove it.

No. I'm not going to prove 2 + 2 = 4, or Pythagoras's theorem either.
They're all standard mathematical theorems, and there's no need.

If you're seriously interested in the proof of the halting problem
theorem (I somehow doubt you really are) have a look at Wikipedia on the
page "Halting problem".

>> > Mr Flibble is very cross at all the laziness in this area of
>> > "research".

>> I note how you put "research" into quote marks, and agree with that
>> totally. The question of the halting problem was completely settled
>> in the 20th century.

> Prove it.

This is getting a bit like a session with a toddler who repeatedly asks
"why?" at the end of every statement or explanation one makes. I can
only redirect you to that same Wikipedia article.

You wouldn't ask for a proof every time somebody says or uses 2 + 2 = 4.
So what is different about the halting problem theorem?

> /Flibble

--
Alan Mackenzie (Nuremberg, Germany).

Jeff Barnett <jbb@notatt.com> writes:

> I was aware the TM + ORACLE* hierarchy has no total halt deciders
> deciders at the same level as the decidee. I was more curious about
> what the axioms might contain to even be able to talk about mechanical
> computations, deciders, and halting. It occurred to be that I had
> never questioned what type of minimal axiomatic support one needs to
> work on these topics.

Ah, I see. Well that's above my pay grade. Here's pretty much all
I know about that:

A TM is just a partial function from state+tape to state'+tape'. The
tape is a function from Z to a finite set, and the state is just a
another finite set. A computation is a sequence (i.e. a function of N)
generated by iterating that function. Halting computations are those
with an end -- an element for which the partial function is not defined.

All of these can be modelled by simple sets, so "all" you really need is
some set theory or other.

Of course, that's a cop out, since set theory is immensely powerful and,
anyway, it's not just one thing -- there are lots of more or less
powerful set theories. And it does no address the question of whether
we need all of the axioms of, say, ZFC, or whether some interesting
subset suffices.

The other way to go would be to find some other axiomatic framework that
is deliberately less powerful than set theory, just to find out what
sort of things are needed as a minimum. This is how we talk about the
reals, for example. Reals can be modelled by sets, so every theorem of
analysis is a theorem of ZFC, but that's not very interesting. Axioms
that capture "just" the parts that matter for a set to be like the reals
are much more revealing.

This is probably what you meant, and I'm sorry I can't say more. I've
seen no work on this, though it may pay to look at proof assistants like
Coq. I know that versions of the hating theorem have been formalised in
some of these frameworks and they will make explicit exactly what axioms
are used and why.

My gut feeling, tough, is that computation and halting are so very
simple that the result of this sort of investigation would not be
particularly interesting.

--
Ben.

On 7/17/2021 2:15 PM, Ben Bacarisse wrote:
> Jeff Barnett <jbb@notatt.com> writes:
>
>> I was aware the TM + ORACLE* hierarchy has no total halt deciders
>> deciders at the same level as the decidee. I was more curious about
>> what the axioms might contain to even be able to talk about mechanical
>> computations, deciders, and halting. It occurred to be that I had
>> never questioned what type of minimal axiomatic support one needs to
>> work on these topics.
>
> Ah, I see. Well that's above my pay grade. Here's pretty much all
> I know about that:
>
> A TM is just a partial function from state+tape to state'+tape'. The
> tape is a function from Z to a finite set, and the state is just a
> another finite set. A computation is a sequence (i.e. a function of N)
> generated by iterating that function. Halting computations are those
> with an end -- an element for which the partial function is not defined.
>
> All of these can be modelled by simple sets, so "all" you really need is
> some set theory or other.
>
> Of course, that's a cop out, since set theory is immensely powerful and,
> anyway, it's not just one thing -- there are lots of more or less
> powerful set theories. And it does no address the question of whether
> we need all of the axioms of, say, ZFC, or whether some interesting
> subset suffices.
>
> The other way to go would be to find some other axiomatic framework that
> is deliberately less powerful than set theory, just to find out what
> sort of things are needed as a minimum. This is how we talk about the
> reals, for example. Reals can be modelled by sets, so every theorem of
> analysis is a theorem of ZFC, but that's not very interesting. Axioms
> that capture "just" the parts that matter for a set to be like the reals
> are much more revealing.
>
> This is probably what you meant, and I'm sorry I can't say more. I've
> seen no work on this, though it may pay to look at proof assistants like
> Coq. I know that versions of the hating theorem have been formalised in
> some of these frameworks and they will make explicit exactly what axioms
> are used and why.
>
> My gut feeling, tough, is that computation and halting are so very
> simple that the result of this sort of investigation would not be
> particularly interesting.

Thanks for the above. The question(s) were in part motivated by the fact
that a lot of the areas where we reason about provable behavior of
computations have developed specialized tools and "logical models". I'm
thinking of complexity analysis of algorithms (mostly a la Knuth "The
Art", not the P =? NP branch), provably secure systems, algorithmic
correctness, etc. So I thought reasoning about abstract concepts like
halting and the boundaries of computational possibilities might have
inspired some interesting tool inventions too. If you ever run into
something fascinating along these lines let us all know!

BTW: The publishers of Linz offer a set of tools to help create and play
with the type of formalisms discussed in the text. Not only are they
free, they are very limited as best I can tell.
--
Jeff Barnett