[net.philosophy] A halting problem: a meaty response

weemba@brahms.BERKELEY.EDU (Matthew P. Wiener) (01/19/86)

In article <3978@kestrel.ARPA> ttp@kestrel.ARPA writes:
>The question of whether or not people are capable of solving the
>Halting problem in general (which, as people have abundantly shown, is
>equivalent to solving your favorite outstanding mathematical problem)

Not so.  Of course, everyone did reply with Fermat's great conjecture,
but that is solely because it is so short and famous.  However, solving
Fermat's conjecture does not solve the halting problem!

>does not seem amenable to a rational answer.

NO is a rational answer.  See me rationalize below.

>                                             Sure there are hard
>problems, but cleverer people pop up over the centuries and solve some
>of the outstanding problems, but then the remaining problems are
>harder, etc.

That etc. is the topic of this response.

There are problems now known which are believed forever insoluble.  In
set theory, there are questions of the form is ZFC + X consistent?  (ZFC
is the most common axiomatization of set theory, X is some statement one
is interested in.)  The statements X one considers are various combina-
torial/large cardinal questions.  It would not be hard to right a program
to loop through all sequences of logical deductions that follow from ZFC+X,
and halt upon getting 0=1.  What is interesting is that the statements
studied have fallen into a nice linear hierarchy.  That is, there are
natural Xs, say X1, X2, ... with (ZFC+X1)'s consistency following from
ZFC+X2, whose own consistency follows from ZFC+X3, etc.

This was all predicted by Godel, but his statements were always ones
which had a naturally agreed upon truth value.  Thus ZFC does not prove
that ZFC itself is consistent, but everyone agrees that it is consistent
(with a few demented exceptions).  And then everyone agrees that the
extended axiom system ZFC + "ZFC is consistent" is itself consistent,
etc.  No matter how many times you repeat this Godelization (finite
or infinite) everyone still agrees that the resulting system is consistent.

What the statements X1, X2, do, however, is transcend this simple iteration,
leading to more and more powerful set theories.  The question is: At what
point do you get inconsistency?  If X135 is inconsistent, then the trivial
program mentioned above can find out for us, and presumably the mathematical
community will find out on its own anyway.  But if it is consistent, then how
would we ever find out???  Again, as soon as we leave the simple Godeliz-
ations, we enter a new and rather queasy mathematical uncertainty.  The first
several levels are generally considered tame, the next tolerable, then they
get rough, and the highest levels are considered quite dangerous, whose true
believers form a cult (it is even centered in LA!).  (There are, I should
mention, various heuristic reasons given for their reasonablenesses.  But that
is the best one can ever do apparently.)

But now comes the amazing part.  The questions are not just relevant to one
particular branch of mathematics.  There is a theorem due to Matiyasevich
which allows one to effectively turn the set theoretic questions into partic-
ular number theoretic questions.  The putative proofs of ZFC + X implies 0=1
correspond to putative solutions to a certain Diaphontine equation. That is,
there are explicit equations (the smallest ones known have ~25 variables),
for which the question of whether they have integral solutions falls in that
spectrum of uncertainty mentioned above.  In fact, it is quite conceivable
that certain problems like Fermat's (or even his conjecture itself!) are of
this form.

Thus, if we consider, not the Fermat loop, but a poly_X loop, where poly_X
is a Matiyasevich-derived polynomial corresponding to axiom X, we get a very
troublesome situation.  When X is one of the tamer propositions, I can assert
that I, and much of the set theory community believes that the poly_X loop
never halts, but so what?  Has our human mind, because of its clever study
of the more powerful statements, realized that X is tame enough, and so it
knows(?) that the loop halts?  That is a rather weak sort of solution, and
falls apart as one climbs the consistency strength hierarchy.  And are there
alien minds whose fundamental mathematical intuition just SEES some ZFC + X
is true the way we see ZFC is true?  (Or even some human minds?)  (As an
aside, the C in ZFC stands for the axiom of choice.  That axiom had a rather
turbulent acceptance period historically, but it is now nearly universally
accepted.  How much have our minds changed in a hundred years?)

The room for unanswerable speculation is very wide here; I find the very
existence of this provably more-and-more-uncertain hierarchy the clincher
in the question of whether the human mind can zap every infinite loop.

>              I suspect that I at least am not capable of solving
>every problem (such humility).

There's no need to suspect! :-)

As Bertrand Russell once noticed, if one first defines a religion as a body of
beliefs depending on faith, then not only is mathematics a religion, it is the
only religion that goes about proving that it is a religion.

ucbvax!brahms!weemba
Matthew P Wiener
UCB Math Dept
Berkeley CA 94720

franka@mmintl.UUCP (Frank Adams) (01/23/86)

In article <11452@ucbvax.BERKELEY.EDU> weemba@brahms.UUCP (Matthew P. Wiener) writes:
>>                                             Sure there are hard
>>problems, but cleverer people pop up over the centuries and solve some
>>of the outstanding problems, but then the remaining problems are
>>harder, etc.
>
>That etc. is the topic of this response.
>
>There are problems now known which are believed forever insoluble.

Just a note here -- this discussion gives examples of problems which are
*believed* forever insoluble.  This is not the same as being *known* to
be insoluble.  There does not seem to be any way to know that a problem
is definitely insoluble (as distinct from undecidable in a formal system).

Frank Adams                           ihpn4!philabs!pwa-b!mmintl!franka
Multimate International    52 Oakland Ave North    E. Hartford, CT 06108

weemba@brahms.BERKELEY.EDU (Matthew P. Wiener) (01/29/86)

In article <1070@mmintl.UUCP> franka@mmintl.UUCP (Frank Adams) writes:
>In article <11452@ucbvax.BERKELEY.EDU> weemba@brahms.UUCP (Matthew P. Wiener) writes:
>>
>>There are problems now known which are believed forever insoluble.
>
>Just a note here -- this discussion gives examples of problems which are
>*believed* forever insoluble.  This is not the same as being *known* to
>be insoluble.  There does not seem to be any way to know that a problem
>is definitely insoluble (as distinct from undecidable in a formal system).

I don't quite understand this note, so I'll try to rephrase it.  Nobody *knows*
whether Peano arithmetic is consistent, but everyone (well, almost everyone :-)
*believes* it is.  If one day someone proves it is not, then everyone will, in
fact, *know* it is inconsistent.  The same comment applies to the higher and
higher axioms of infinity I discussed in the >> article, with a spectrum of
lower and lower confidence/reasonableness/Anschauung/?????? in the axioms.

My misunderstanding (have I just expanded his note??) seems to come from the
mere existence of the note.   "this discussion gives examples of problems
which are *believed* forever insoluble" -- can anyone give me an example of
a discussion, *any* discussion, where one *knows* as opposed to *believes*??
(Cf. Lewis Carroll's version of Achilles and the Tortoise.)

ucbvax!brahms!weemba	Matthew P Wiener/UCB Math Dept/Berkeley CA 94720

gsmith@brahms.BERKELEY.EDU (Gene Ward Smith) (01/29/86)

>I don't quite understand this note, so I'll try to rephrase it.  Nobody *knows*
>whether Peano arithmetic is consistent, but everyone (well, almost everyone :-)
>*believes* it is.  If one day someone proves it is not, then everyone will, in
>fact, *know* it is inconsistent.  The same comment applies to the higher and

  Actually, I know the Peano axioms are correct, because the integers are
a model for them. So there!
 

   Gene Smith

ladkin@kestrel.ARPA (01/29/86)

(wiener)
> >There are problems now known which are believed forever insoluble.
> 
(adams)
> There does not seem to be any way to know that a problem
> is definitely insoluble (as distinct from undecidable in a formal system).

There are theorems such as Kruskal's, the Paris-Harrington
version of the Ramsey Theorem, and Friedman's various principles
that are provable stronger than the generally acceptable
principles of arithmetic, and recursive set theory. They are
arguably consistent, since there are `proofs' of them. 
These proofs must depend upon stronger principles than all
mathematicians are willing to accept (e.g. intuitionists).
If you believe these proofs, you will nevertheless be
unable to persuade those who are sceptical of their validity,
and furthermore, there is a proof of this fact.

This point is even valid for Peano Arithmetic.
If you believe that Peano Arithmetic is consistent, as I do,
then there is a proof that proving the consistency of P.A.
from elementary principles is an insoluble problem. 
This is different from deciding the 
consistency of P.A. If you believe Gentzen's proof, as I do,
then the consistency is already decided.

The conclusion I suggest is that:
 Given the FACT that a mathematical principle is undecided by
some formal system, then you would conclude that the consistency
of the principle is an unsolvable problem 
IF EITHER 
you see reason to doubt the principle, but believe it 
consistent nevertheless,
OR 
if you believe the principle.

Hence whether a problem is provably insoluble depends upon the
entirety of the mathematical principles you are willing to accept
as valid.

Peter Ladkin

ladkin@kestrel.ARPA (01/30/86)

In article <11590@ucbvax.BERKELEY.EDU>, gsmith@brahms.BERKELEY.EDU (Gene Ward Smith) writes:

>   Actually, I know the Peano axioms are correct, because the integers are
> a model for them. 

Gene, was this a serious comment? (I presume you mean the natural
numbers, not the integers). If so, this is circular reasoning,
(which, although logically sound, is epistemologically unhelpful).

Peter Ladkin

ttp@kestrel.ARPA (01/30/86)

In article <4374@kestrel.ARPA>, ladkin@kestrel.ARPA (Peter Ladkin) writes:

> There are theorems such as Kruskal's, the Paris-Harrington
> version of the Ramsey Theorem, and Friedman's various principles
> that are provable stronger than the generally acceptable
> principles of arithmetic, and recursive set theory. They are
> arguably consistent, since there are `proofs' of them. 
> These proofs must depend upon stronger principles than all
> mathematicians are willing to accept (e.g. intuitionists).
> If you believe these proofs, you will nevertheless be
> unable to persuade those who are sceptical of their validity,
> and furthermore, there is a proof of this fact.

Summary as I understand it so far:

I first asked whether, assuming that the human race had the computational
power of a Turing machine, that it followed that there was some
PARTICULAR problem (e.g. a halting problem) that could be EXHIBITED
that could never be "decided" by the human race, that is, no one would
ever come along with a proof that the particular machine
would or would not halt. Matt Wiener and Peter
Ladkin have contributed various mathematical problems such as:

 initialize generator of consequences from the Peano axioms;
(loop
  c := the "next" consequence of Peano axioms
  if c is equal to `false' 
     then exit
     else continue)

This program halts if the Peano axioms are inconsistent, otherwise
loops forever.  If this program ever halts, we'll know the axioms are
inconsistent (you with Cray's out there, take note -:). But how could
we justify to ourselves that this program doesn't halt? Most people
assume the Peano axioms are consistent; this cannot however be proved
within the Peano axioms -- and known "proofs", e.g.Gentzen's proof
requires that one appeal to "higher" principles (transfinite induction
up to some large set) that not all mathematicians accept. And even if
you're not as radical as the intuitionists, and accept these proofs, Matt
produced other problems that are even more difficult to intuit.

So my first idea that there come to be cleverer people over the years
who think up new ways to combine existing FACTS and will eventually be
able solve everything is wrong. The kind of insight that such people
have is not a consequence of deduction from existing facts, but rather
to intuit new PRINCIPLES which at least some schools of mathematical
thought will gradually accept. And Peter has pointed out that if such
a principle proves the goal statement you'd like to show, then it is
stronger than the goal, so such a proof only really assumes something
stronger than the original goal to be proved.

The thing I NOW wonder about is from where these principles arise.  I
expect the philosophers will now enter the fray if they are not too
appalled by my naivete, perhaps waving appropriate references ("the
philosophy section of the library" -:).  Assume people have
computational power reducible to Turing machines (ignore
finite/infinite memory). People are, however, situated in the world,
and this may be able to give (some of) them (somehow) glimpses of
infinity.  Where did the Peano axioms come from in the first place?
Perhaps the world somehow interacts with (some) people so as to be a
sort of oracle, where certain undecidable-from-a-formal-theory
consequences become known as intuitively obvious (e.g. the joke about
the Peano axioms are consistent because obviously the natural numbers
are a model).  Also it is known that some great (and not so)
mathematicians intuit truth without at first being able to construct
any formal proof.  This could of course mean that they're simply
working in some better formal system than whatever "formal proof"
means. Or it could mean they see something that would have been
impossible to jump too unless they had interacted with the world. The
world, one expects, is a model of truth.  We've evolved evolutionarily
to embody an understanding of certain principles (Hume?).

Perhaps armed with world experience and some INDUCTION axioms (I'm
thinking of Doug Lenat's EURISKO work here), people can concoct higher
and higher truths. Or it could be that we're stuck at some large
cardinality set, and as Matt implied, we'll have to wait for the
answers from some other race with a "higher" intuition.

-tom

Note: "experience with the world", I assume, is finite, so induction is
necessary to generate any infinite consequences.

franka@mmintl.UUCP (Frank Adams) (02/04/86)

In article <4374@kestrel.ARPA> ladkin@kestrel.ARPA writes:
>(wiener)
>> >There are problems now known which are believed forever insoluble.
>> 
>(adams)
>> There does not seem to be any way to know that a problem
>> is definitely insoluble (as distinct from undecidable in a formal system).
>
>There are theorems such as Kruskal's, the Paris-Harrington
>version of the Ramsey Theorem, and Friedman's various principles
>that are provable stronger than the generally acceptable
>principles of arithmetic, and recursive set theory. They are
>arguably consistent, since there are `proofs' of them. 
>These proofs must depend upon stronger principles than all
>mathematicians are willing to accept (e.g. intuitionists).
>If you believe these proofs, you will nevertheless be
>unable to persuade those who are sceptical of their validity,
>and furthermore, there is a proof of this fact.
>
>This point is even valid for Peano Arithmetic.
>If you believe that Peano Arithmetic is consistent, as I do,
>then there is a proof that proving the consistency of P.A.
>from elementary principles is an insoluble problem. 
>This is different from deciding the 
>consistency of P.A. If you believe Gentzen's proof, as I do,
>then the consistency is already decided.

But if you do *not* accept the postulate, that means you are in real
doubt about it.  That, in turn, means you don't know whether or not
it is undecidable.  Because if Peano Arithmetic is not consistent,
then there actually exists a counterexample, which can be demonstrated.
You can, perhaps, know that someone else's problem is unsolvable *by
them*, but you cannot know the same for yourself (for this class of
problems, at least).

Frank Adams                           ihpn4!philabs!pwa-b!mmintl!franka
Multimate International    52 Oakland Ave North    E. Hartford, CT 06108