Re: FOL, ZFC, NGB and Prolog

Keith Ramsay wrote:

>

Dear Mr Ramsay,
Thank you very much indeed for writing. Please, kindly be assured - I
know you are right, and I have full confidence in your words. *I DO*.

> |Sir, thank You very much indeed for all Your kind comments. You have
> |been most helpful to me, I dare say I would not have made _any
> progress
> |whatsoever without the information You kindly provided. *IF* this is
> |not too much to ask, and *IF* you think I deserve it, please kindly
> |grant me _only the three letters. Oh, please.
>
> There's no need for talk about whether you deserve it,
> capitalizing "you" and so on. Whatever information you
> might need is surely available if you're willing to
> take the time to digest it for yourself.

I agree.

> With access to a good college library, people to help you
> are not necessary or sufficient.

I see. Still, how do you suggest anyone digest the Church-Turing thesis
without being solicited by a TRULY authoritative tutor with *vast*
experience? I myself glanced over Turing's work on intelligence several
times, and thought the ideas impossible. This has to do with a cultural
background. Still more, I fail to recall who said that we learn by
sitting at the feet of our gurus?

> Don't act more dependent than you are.

Affirmative.

> You referred to wanting to implement ZFC in Prolog and
> put it into a "pattern matching" framework. This is all
> a little vague. Try to be a little more specific about
> what you really want to accomplish.

I have been as specific as possible. I asked the question, answered it,
and asked to be solicited. My problem is that I will not make _any
progress unless I am granted the three letters by Other Posters. I
apologize to each and every participant of this fine NG for being such
a nuisance (please, kindly see the last clause of this post).

> Formal systems such as ZFC are related to computation in
> the sense that the theorems of ZFC are computable enumerable.
> I only have a general idea of what Prolog is like, but I
> gather it's a universal language, so one could implement a
> prolog program that enumerates the theorems of ZFC. It's not
> clear whether this will do for you anything like what you
> want to do. It might be an interesting exercise in understanding
> first-order logic and practicing Prolog programming. It's very
> unlikely that running the program will in practice generate
> any theorems of interest. I don't know whether Prolog even
> has any language features that would make this easier to do
> or work better than in some more general purpose language.

Mr Ramsay, I comprehend and agree with you fully.

> The problem is essentially the same as with any other kind of
> exhaustive search. We could write a program that would eventually
> produce all the sonnets of Shakespeare, *in principle*, just by
> going through all the possible combinations of characters up to
> a maximum length, but the time required would be so long that in
> fact one wouldn't get any of them before the Sun burns out.
>
> For a program that searches for deductive consequences of a set
> of axioms to be more than a theoretical exercise, it has to be
> "smart" about what combinations of deductive steps it tries out.
> A lot of work has been done attempting to devise algorithms for
> searching for proofs of theorems, but obviously it's only gotten
> so far at this point. If it becomes more efficient to get a
> computer to find a proof than to get a mathematician to do it,
> not just in certain limited areas of mathematics but generally,
> I'm pretty sure we'll hear about it.

Yes, Mr Ramsay.

> Having said all this, I have little confidence that this is what
> you're looking for. You've been very nonspecific. Prolog, ZFC,
> pattern matching... all fine, but what is it that you're really
> after?

I am after truth, i.e. pure mathematics.

Thank You.
Tom

.