Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.theory > #36461 > unrolled thread

HP undecidability is not an axiom

Back to article view | Back to comp.theory

Contents

  HP undecidability is not an axiom Mr Flibble <flibble@reddwarf.jmc> - 2021-07-16 22:33 +0100
    Re: HP undecidability is not an axiom olcott <NoOne@NoWhere.com> - 2021-07-16 17:02 -0500
    Re: HP undecidability is not an axiom Ben Bacarisse <ben.usenet@bsb.me.uk> - 2021-07-16 23:21 +0100
      Re: HP undecidability is not an axiom Jeff Barnett <jbb@notatt.com> - 2021-07-16 16:48 -0600
        Re: HP undecidability is not an axiom Ben Bacarisse <ben.usenet@bsb.me.uk> - 2021-07-17 00:11 +0100
          Re: HP undecidability is not an axiom Jeff Barnett <jbb@notatt.com> - 2021-07-16 23:07 -0600
            Re: HP undecidability is not an axiom Ben Bacarisse <ben.usenet@bsb.me.uk> - 2021-07-17 21:15 +0100
              Re: HP undecidability is not an axiom Jeff Barnett <jbb@notatt.com> - 2021-07-17 17:30 -0600
    Re: HP undecidability is not an axiom Alan Mackenzie <acm@muc.de> - 2021-07-17 12:00 +0000
      Re: HP undecidability is not an axiom Mr Flibble <flibble@reddwarf.jmc> - 2021-07-17 13:03 +0100
        Re: HP undecidability is not an axiom Alan Mackenzie <acm@muc.de> - 2021-07-17 12:30 +0000

#36461 — HP undecidability is not an axiom

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

[toc] | [next] | [standalone]

#36464

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

[toc] | [prev] | [next] | [standalone]

#36469

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.

[toc] | [prev] | [next] | [standalone]

#36475

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

[toc] | [prev] | [next] | [standalone]

#36480

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.

[toc] | [prev] | [next] | [standalone]

#36495

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

[toc] | [prev] | [next] | [standalone]

#36565

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.

[toc] | [prev] | [next] | [standalone]

#36571

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

[toc] | [prev] | [next] | [standalone]

#36504

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).

[toc] | [prev] | [next] | [standalone]

#36505

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

[toc] | [prev] | [next] | [standalone]

#36506

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).

[toc] | [prev] | [standalone]

Back to top | Article view | comp.theory

csiph-web