Re: FOL, ZFC, NGB and Prolog


Tom wrote:
|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. With access
to a good college library, people to help you are not
necessary or sufficient. Don't act more dependent than
you are.

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.

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.

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.

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?

Keith Ramsay

.

Relevant Pages

  • Re: FOL, ZFC, NGB and Prolog
    ... Dear Mr Ramsay, ... > 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, ...
    (sci.logic)
  • Re: Continuum hypothesis
    ... ZF" or "theorems of PA compiled into ZF"? ... Statements in "The 2nd-order language of arithmetic", however, do not ... order ZFC, and models that are nonstandard in other ways as well. ... It seems to me that first-order PA is strong enough to code ...
    (sci.logic)
  • Re: Continuum hypothesis
    ... ZF" or "theorems of PA compiled into ZF"? ... the axiom of infinity. ... Statements in "The 2nd-order language of arithmetic", however, do not ... order ZFC, and models that are nonstandard in other ways as well. ...
    (sci.logic)
  • Re: Rational numbers, irrational numbers: each dense in real numbers
    ... That's all the theorems about those ... inconsistent theorems, then the collection of consistent theorems ... ordinals, to be "the union restricted to i and i is an ordinal", ... ZFC, because there is no universe in ZFC. ...
    (sci.math)
  • Re: Rational numbers, irrational numbers: each dense in real numbers
    ... proved certain theorems about theories. ... class in ZFC with classes instead of a set in ZFC, ... trivial theories are obviously consistent and complete, ... consistent and inconsistent, then they can't be separated, else there ...
    (sci.math)