Re: .EXE -> .ASM -> .EXE


Charles A. Crayne wrote:

:A problem whose language is recursive is said to be decidable.
:Otherwise the problem is undecidable. That is, a problem is undecidable
:if there is no algorithm that takes as input an instance of the problem
:and determines whether the answer to that instance is yes or no.

Since the language of the two examples of the "liar's paradox" which I
posted is clearly NOT recursive, and you have made no attempt to show
that there is an algorithm which will determine either the truth or the
falsity of the statements, then by your own citation, they must be
undecidable.

Ah, but the second paragraph which you left out answers this dilemma:
specifically:

func1: return true;

func0: return false;

One of these functions (which are algorithms, as they halt and return
an answer) most certainly returns the answer. Here's the rub: these two
functions exist *outside* the context of those two statements you gave.
That is, they require knowledge gleened from outside the universe of
those individual statements.


Raymond Smullyan, in his book "Forever Undecided" says the
same thing in more formal terms, "A proposition p is said to be
"undecidable" in a system S if neither it nor its negation ~p is provable
in S".

Well, I won't wander into the field of propositional logic, because I
my training in that area consists of a single undergraduate philosophy
course, so I would be treading dangerous waters to act the expert
there. So the best I can do is say that I'm not *sure* that the concept
of undecidability in propositional logic is quite the same as it is in
Computer Science. Howeverl let's assume that it is.

First of all, we know that if a language is recursive (and therefore
decidable), then the same is true for its complement (negation). The
proof is rather simple (see Hopcroft and Ullman). Basically, if "f(x)"
is recursive, then we can use the algorithm "not f(x)" to compute the
complement of the function (and this will always halt, etc., etc.).
IOW, the "nor" in the statement above is redundant if that statement in
propositional logic *does* map exactly to the concept of undecidability
in Computer Science. Therefore, it concerns me somewhat that this
clause is even present.
I wouldn't know how to map "is provable" in propositional logic to "is
recursive" in computer science, though.


What surprises me is that you, who claim to have learned "about these
types of things", are not aware that this paradox was first raised in
Greece about 2600 years ago, and -- far from being dismissed as trivial --
has been taken very seriously by most reputable mathematicians.

Again, you're confusing computability with decidability.


But the key point is that yet another formulation of this same paradox is
the prime factor in Godel's proof of his First Incompleteness Theorem. So,
until one truly understands the paradox, one cannot possibly understand
Godel's works.

And what you need to understand is that decidability does not equal
computability.

When I get home tonight, I'll dig out Hopcroft and Ulman again and give
you the classic example of a uncomputable function, which is roughly
equivalent to your proposition B

Cheers,
Randy Hyde

.

Relevant Pages

  • Re: A question on GIT.
    ... Maybe you're confusing truth with provability -- or something like that. ... Decidability is a question of what you can prove in a system, ... proof of its undecidability. ...
    (sci.logic)
  • Re: Godels comments about the "true reason" for incompleteness
    ... arbitrary Q. Obviously there is an implied quantification over Q, ... letters of the object language). ... we want to convey that "all" propositions follow from a contradiction. ... refutable in PA and as confirmed by the supposed undecidability of S. ...
    (sci.logic)
  • Re: Godels comments about the "true reason" for incompleteness
    ... principles regarding formal sentences result in theories synonymous, ... We now perform a mutual translation as follows. ... expressible in the language of T into the language of PA. ... Similarly the undecidability of in T ...
    (sci.logic)
  • Re: Question on Conservative Extensions
    ... undecidability and they state assumptions in two ways. ... T' is a finitely axiomatizable theory of L', ... Let L be a language with just finitely many non-logical symbols and Let ... where c is an individual constant symbol not in L. Let S ...
    (sci.logic)