Re: ZFC
- From: examachine@xxxxxxxxx
- Date: 5 Jul 2005 05:55:08 -0700
Torkel Franzen wrote:
> examachine@xxxxxxxxx writes:
>
> > First, there is a long running tradition that constructive proof =
> > algorithm.
>
> This is a misunderstanding. There is no such tradition. A
> constructive proof of an AE-statement yields an algorithm, but this
> does not imply that an algorithm is a proof of anything.
I don't believe this is the prevailing opinion among mathematicians.
The statement yields a unique algorithm. And guess what, the reverse
direction works too. So you got an identity there.
Also note that I said I held this assumption without the intricacies.
I would have to discuss these if I had to convince skeptics as
yourself.
Anyway, you probably won't be willing to learn anything new, so...
> > This means that I simply have to present a pseudo code. And *that*
> > is the proof.
>
> Proof of what? Returning to the example of the commutativity of
> addition, you have apparently expressed the idea that an algorithm for
> computing x+y is at the same time a proof that x+y=y+x for all inputs
> x,y. Since this is so obviously absurd, let us assume that it is not
> what you intend to claim. So just what presenting of pseudo code is it
> you have in mind as a way of proving that addition of natural numbers
> is commutative?
You definitely do not understand a thing that I say. The
programs in this case are nothing but programs which manipulate
other programs. I think you can work out an example if you know
a bit of lambda calculus. It is sufficient for each of the claims
that you demonstrate a single program that does the job. There is
no further proof-work involved.
This is basically how we can be intelligent at all: programming.
McCarthy figured this out in the 1950s. 50 years later "professional"
logicists still don't understand what lambda calculus is. But worry
not. We are quite close to the computational capacity needed to let
machines write their own programs. It is only a matter of time, now.
You can also try a little information theory which might let you
program "in the abstract" to prove the same fact. Chaitin could prove
interesting things using that method.
You probably want me to write again technical explanations for a couple
of pages, to which you will write irrelevant objections, effectively
wasting my CPU time. I won't fall for those ploys any more.
Bored,
--
Eray
.
- Prev by Date: Re: ZFC
- Next by Date: Re: ZFC
- Previous by thread: Re: ZFC
- Next by thread: Re: ZFC
- Index(es):
Relevant Pages
|
