Re: ZFC

In article <42a44a5b$0$567$b45e6eb0@xxxxxxxxxxxxxxxxxxxxxxxxx>,
tchow@xxxxxxxxxxxxx wrote:

> In article <haberg-0606051004590001@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx>,
> Hans Aberg <haberg@xxxxxxxxxx> wrote:
> >I got into the subject by writing on a theorem prover, based on extending
> >and adapting a Prolog program using Hilbert's axioms, even though the
> >underlying computational engine does not have any such limitations. Then I
> >cross into those questions of metamathematical type theory, higher order
> >theories and such, and it is not very clear what to use as basis.
>
> Well, this much is certainly true, but it's misleading to express
> this concept by saying "the foundations of mathematics are unclear."
> To say that the foundations of mathematics are unclear suggests that the
> subject is obscure and is plagued by logical difficulties that people
> don't understand very well and are still trying to clarify.

When the subject has cleared up, one will be able to settle on a sngle
theory. That has not happened yet.

> That's very
> different from saying that for the purposes of building a theorem prover,
> there are many choices and no clearcut winner.

If the approach is right, the theorem prover will only implement the
theory straight on.

> When building a theorem
> prover, one has to consider many issues such as efficiency, ease of use,
> peculiarities of the particular problem domain of interest, elegance,
> and so forth.

This what computer scientists generally do, often dictated by practical
concerns, and the lack of a general theory to make use of, the one
mathematicians have not yet settled on.

But this is not something one has to do. I decided to not follow that
approach, simply because I want to investigate the formal math aspect. I
have put in stuff, usually not used by computer people, based on what is
actually used in formal theories. For example, among other things, I have
attained automated induction proofs, done via a breadth first search, so
that if there is a finite proof, it will be found. Very disappointing,
because students using it will never learn what an induction proof is. :-)

> The same goes for investigations into alternative foundations for
> mathematics besides ZFC. The existence of these investigations doesn't
> mean that there's anything logically suspect about ZFC. But depending
> on what your goals are, you may find some other approach more natural,
> elegant, efficient, etc.

As soon as a consistent theory will have been put forth, we will know for sure.

--
Hans Aberg
.

Relevant Pages

  • Re: Complete Arithmetic?
    ... >Building automated theorem prover is a great challenge, ... >Genetic programming can be regarded as a buzzword. ... on to unsolved mathematics... ...
    (sci.logic)
  • Re: ZFC
    ... >I got into the subject by writing on a theorem prover, ... To say that the foundations of mathematics are unclear suggests that the ... mean that there's anything logically suspect about ZFC. ...
    (comp.theory)
  • Re: the error in Godels proof
    ... tell us more about this theorem prover. ... Moving mathematics forward is exactly why Godel's ... to calculation, ... Theorem with your own standard of usefulness, ...
    (sci.math)