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

Groups > comp.theory > #36565

Re: HP undecidability is not an axiom

Show all headers | View raw

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.

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