Re: Computability and logic
- From: "george" <greeneg@xxxxxxxxxx>
- Date: 30 Sep 2006 08:01:37 -0700
Tom wrote:
I was just thinking I am really
trying to establish what Goedel's Bew(x,y) really is, you know.
It's just a defined binary first-order predicate.
In Godel's original it was in the language of PM but
for our purposes it would be in the first-order language of
Peano Arithmetic. If you use FOL with equality and 1 instead of s(.)
then this is a VERY simple language; its only terms are 0 and 1
and what you can build from them with + and x . It doesn't have
or need any predicates at all (since = is already built-in).
But because that makes most statements in it every bit as
unreadable as machine language (compiled into 0's and 1's),
there is a mechanism for adding DEFINED predicates and functions.
E.g. less(x,y)<=df=>Ez[(x+1)+y=z], or
prime(x)<=df=>Ayz[ less(y,2)v less(z,2)v less(x,y)v less(x,z)v
~(y*z=x)]
Just as prime is defined in terms of less, here Bew is defined in terms
of a high tower of other things that were defined earlier. But it is a
NUMERIC
function. Strings are NOT actually involved here except to the extent
that
(1 + (1 + (1+ (1 + 0 )))) is a string (which it isn't, actually; it's a
term).
I mean, I am trying to reach a single string which incorporates both the
starting sequences and the rules of inference (Bew) from the inside,
You don't have to "reach" Bew; it was already defined in Godel.
which is impossible.
Given that it's been done, it can hardly be impossible, unless you are
saying
that it was done in some non-string way, and what you are trying to do
is
translate it into a string. But again, the framework is PA, is
NUMBERS, NOT
strings. Why would you be trying to redo FOL where the whole framework
is strings and not terms? Aren't terms plenty string-like enough
already?
If you can finesse the difference between a character and a
string-of-length-1,
you can already articulate some simple axioms about how strings work.
But, again, if it is impossible how we do that at all?
I'm losing your antecedents of "it" and "that" here.
I mean, given a TM description and a tape, how do you apply the
description to the tape to obtain another tape. Don't you need a meta,
and meta-meta, and meta-meta-meta ... machine to do that?
Well, no, me, personally, I don't. I can just look at it.
You do.
No, I don't. The fact that there is a TM that can confirm for me
that the string II concatenated with the string III yields the string
IIIII
does NOT mean that I *need* this TM *before* I can do that.
*My* brain is Turing-equivalent modulo finitude (despite the
fact that Turing was a lot smarter than I am).
More to the point, mathematical functions in general don't "need"
a TM-implementation *before* they can operate; they just operate
on their arguments and produce the results they produce from them.
Instantaneously. For all arguments. IN PARALLEL. IN AETERNAM.
Still, we manage to do the thing. How?
I didn't realize how old your question was.
In the popular literature, this question occurs in
Hofstadter's "Godel, Escher, Bach" in the context of
how we determine that inference rules are sound.
If we know P is non-contradictory, if we know
P-Q is true, and we know modus ponens is sound,
then, yes, we can infer Q, but how do we know that
all the machinery we used in making THAT inference was sound?
We can prove by truth-tables that
If we have P, and we have P->Q, then we can infer Q.
But how do we know that the truth-table method is sound?
Don't we need some further justification for that?
Hofstadter is continuing a thread begun by Lewis Carroll
in "What the Tortoise Said to Achilles" some 80 years prior.
If you have children then one of them may at some point
around age 4 have gotten into the habit, once you
gave an explanation in response to a question of type
"Why?", of iterating the question: "Why?"
There is in principle no end of that.
That is what AXIOMS are for.
At some point you can have to be able to say that
you can tell ad oculos, by inspection, that something
matches a pattern that makes it acceptable by fiat,
just because we said so, just because we agreed NOT
to seek DEEPER justification for things of THAT shape.
This raises 2 concerns. Either 1) we might be mistaken
in recognizing the thing as matching the pattern (this is
why axiom-sets have to be recursive, and why proof-predicates
have to be PRIMITIVE-recursive), or 2) the reasoning might
actually BE unsound and might lead us to accept something
contradictory. In the case of first-order logic we rebut this
objection by simply pointing out that since it is complete
(the LOGIC, NOT a rich theory IN it) and since first-order
consequence is r.e., then if we have accepted something that
entails a contradiction, WE CAN PROVE that eventually, and
thus evolve away from the contradiction.
The problem in any case is NOT about "producing" strings or tapes.
TMs are thought of as just "having" their programs inside them
somewhere, as you might know the recipe for baking a cake.
The fact that the recipe can also be written down in a cookbook
does NOT imply that you have to know how to read before you can
know how to bake a cake.
.
- Follow-Ups:
- Re: Computability and logic
- From: Tom
- Re: Computability and logic
- References:
- Re: Computability and logic
- From: Tom
- Re: Computability and logic
- Prev by Date: how to prove ~ ( P & Q) => ~P v ~Q
- Next by Date: Re: how to prove ~ ( P & Q) => ~P v ~Q
- Previous by thread: Re: Computability and logic
- Next by thread: Re: Computability and logic
- Index(es):
Relevant Pages
|
Loading
