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

Groups > comp.theory > #36571

Re: HP undecidability is not an axiom

Show all headers | View raw

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

Back to comp.theory | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

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

csiph-web