Re: A little knowledge is a dangerous thing - THE HALTING PROOF

On May 5, 9:15 pm, Charlie-Boo wrote in sci.logic:

CB>> 1. There is a way ("effective") that is not an algorithm. ... 2.
There is a different way for each number, but no single way for all
numbers. ... But maybe he can explain a little better than I can with
my guesses. <<CB

Charlie
=======
Thanks for clarifying the issue with some incisive comments and
analysis.

In footnote 36 of 'Some consequences of defining mathematical objects
constructively and mathematical truth effectively', I clarify that:

"In other words, we argue that not every effective method is
necessarily algorithmic, although every algorithm is an effective
method. The possibility that "truth" may be non-algorithmic, and
yet constructive, is implicit in Gödel's famous 1951 Gibbs lecture
[Go51], where he remarks:

'I wish to point out that one may conjecture the truth of a universal
proposition (for example, that I shall be able to verify a certain
property for any integer given to me) and at the same time conjecture
that no general proof for this fact exists. It is easy to imagine
situations in which both these conjectures would be very well founded.
For the first half of it, this would, for example, be the case if the
proposition in question were some equation F(n) = G(n) of two
number-theoretical functions which could be verified up to very great
numbers n.' "

In footnote 98 I observe, further, that such a possibility is also
implicit in Turing's remarks ([Tu36], §9, para II):

"Let P be a sequence whose n-th figure is 1 or 0 according as n is or
is not satisfactory. It is an immediate consequence of the theorem of
§8 that P is not computable. It is (so far as we know at present)
possible that any assigned number of figures of P can be calculated,
but not by a uniform process. When sufficiently many figures of P have
been calculated, an essentially new method is necessary in order to
obtain more figures".

Now, in his seminal 1931 paper, Goedel constructs an arithmetical
relation R(x), and gives a constructive, and intuitionistically
unobjectionable, meta-proof that the formula [R(n)] is provable for any
given numeral [n] in any formal Peano Arithmetic, and that the formula
[(Ax)(R(x)] is not provable in the Arithmetic.

Prima facie, using Occam's razor, a straightforward interpretation of
this is that the arithmetical relation R(x) is effectively verifiable
instantiationally, but that it is not uniformly (i.e., algorithmically)
verifiable - hence it is not Turing-computable.

Such an interpretation would, of course, need to appeal to a
provability thesis such as:

Provability Thesis (PT): A true arithmetic relation is
Turing-computable, when treated as a Boolean function, if, and only if,
it is PA-provable.

As a consequence of Turing's Halting Theorem, the thesis is essentially
unverifiable. We are thus at liberty to either adopt it or to deny it.

Although classical theory does not appear explicitly committed to
either case, standard interpretations of classical theory - including
Goedel's own (implicitly Platonic, and arguably non-constructive)
interpretations of his formal reasoning - do seem to conflict with the
thesis.

In my above paper, however, I consider a constructive interpretation of
classical theory in which PT follows as a consequence of some more
fundamental theses.

Consequently, Goedel's reasoning would interpret as a constructive
proof that R(x) is effectively true instantiationally, but that it is
not Turing-computable.

It could, thus, be described as an instance of an effective method that
ensures the effective verifiability of the truth of a denumerable set
of arithmetical propositions, without recourse to an algorithm.

Regards,

Bhup

.

Relevant Pages

  • Re: arithmetic in ZF
    ... By At Home, I mean, IN NATURAL LANGUAGE! ... Rbut there is no ONE algorithm that does them ... and there is NO interpretation of ANYthing ... What makes something a predicate is ...
    (sci.logic)
  • Re: arithmetic in ZF
    ... Goedel's reasoning can be taken to establish that ... well-defined under an interpretation M, ... In the absence of such an algorithm, we may still have that, for any s ...
    (sci.logic)
  • Re: rounding
    ... that Bob didn't explicitly say that the interpretation alluded to was ... TITLE: Evaluation of Intrinsic Procedures ... When the standard specifies an algorithm for computing a ...
    (comp.lang.fortran)
  • Re: Riemann Hypothesis and P vs NP
    ... >> Right, but the correctness of the algorithm I mentioned, did. ... Miller-Rabin runs in polynomial time. ... that my interpretation was the natural one. ...
    (sci.math)
  • Re: Riemann Hypothesis and P vs NP
    ... >> Right, but the correctness of the algorithm I mentioned, did. ... Miller-Rabin runs in polynomial time. ... that my interpretation was the natural one. ...
    (comp.theory)