Re: proof of undecidability of halting problem

Jan Burse wrote:

No, a turing machine has no formulas in it.
And a turing machine amounts to a formula

No, a turing machine has no formulas in it.

of the form exists x P(x), where P has
bounded quantifiers.

> The difference is in the base, YES(a,b) =
> "TM a halts yes on input b." and PR(a,b) =
> "Wff a with b substituted for its free
> varable is provable."

provable in which logic? PR can express
more than YES.

How does YES express anything? It only represents things (r.e. sets.)

Not recognizing how to use Predicate Caluculs
> wffs to express database queries, file
> structures, programming requirements, assertions
> in the Theory of Computaton and in Incompleteness
> in Logic is one of the basic failings of conventional
approaches.

What do you mean by "conventional approaches"?

Published by stupid college professors who ok each other's papers. (It
shows you what inbreeding produces.) If they were computer
programmers, then they couldn't BS their way through. Their systems
(computer programs) would have to work for real.

That a turing machine has the form exists x P(x)
is not "conventional", its an insight about
computability. And database queries, file
structures, assertions, all have also this
form exists x P(x), as long as they are computable.

But representing it using Predicate Calculus is what is missing from
conventional wisdom. Read any book on database, Theory of Computation,
Program Synthesis.

But wffs go beyond computability, namely for
example the arithmetical hierarchie, so why
should this be "conventional".

What is the requirement for an axiomatic system to be such that the
theorems of Godel (1931), Rosser (1936), Turing (1937) and Smullyan
(1960-present) apply?

The sentences of Gödel, Rosser, Turing, Smullyan
can be classified in the arithmetical
hierarchie.

You are not stating the conditions under which these theorems apply to
a particular Logic. Each theorem has a different condition. Everyone
says "Rosser used a more complex wff than Godel and achieved a stronger
result." That is not true. He has a different requirement on the
Logic. Sometimes Godel's results apply but Rosser's doesn't.
Formalizing shows this.

C-B

Bye

.

Relevant Pages

  • Re: Theory of programming
    ... All trivial-input programs have an equivalent Turing machine ... > modern programming. ... computer science which isn't in my mind efficiency it is correctness. ...
    (comp.programming)
  • Re: Itanium had appeal
    ... A misbegotten imaginary generalization of the Turing machine is at the ... I, personally, blame the vonNeumann programming model. ... One could say the same about LISP programs....or the purporters of ...
    (comp.arch)
  • Re: Itanium had appeal
    ... we'll recognize a Turing machine as an interesting ... I, personally, blame the vonNeumann programming model. ... The God-awful trick that computer scientists call non-determinism ...
    (comp.arch)
  • Re: What is a programming language?
    ... >>Or, said otherwise, the interpreter of HTML IS NOT a Turing Machine ... > No programming language is a turing machine and no existing ... Show me an interpreter for HTML written in HTML! ...
    (comp.lang.lisp)
  • Re: The Impossibility of Proving the Truth Set Productive
    ... generate all the theorems of T. ... If you find that NHis a theorem of T, then halt. ... Let k be the index of the Turing machine M_k that computes f_T. ... axiomatic system to this wff. ...
    (sci.logic)