Re: Definition of Functions in Calculus

Herman Rubin wrote:
> In article <4b4d3$42d77ce0$82a1e3ad$28770@xxxxxxxxxxxxxxxx>,
> Han de Bruijn <Han.deBruijn@xxxxxxxxxxxxxx> wrote:
>
> >English and all other "common languages" have been precise enough to
> >serve mankind for centuries. So show more respect in the first place.
> >And BTW, common speech is still the main vehicle for proving theorems
> >in mathematics, instead of what you might expect: formal logic.
>
> [ ... ]
> Theorems in mathematics are supposed to be provable with formal
> logic, and most mathematicians are aware of this. If one uses
> the procedure known as Natural Deduction, most proofs will not
> lengthen by more than a small factor, and a machine will be able
> to check the correctness. The elision in using "common language"
> to prove theorems is essentially asking the reader to insert
> some of the formal steps, and that part of the language still
> has different meanings for mathematicians than for others.

I think you are referring to a computer program like AUTOMATH, which
has
been developed by N.G. de Bruijn (not a relative of mine) and his crew.

Now I wonder if i.e. Wiles' proof of Fermat's Last Theorem has been
checked out by such a program. I'm almost certain the answer is: NO.

So what's the beef, if formal logic doesn't actually replace common
speech reasoning, not even in situations where such a thing would be
highly desirable? I mean for the truly difficult proofs ...

Han de Bruijn

.

Relevant Pages

  • Re: Godel proved maths inconsistent not incompleteness theorem
    ...  It's the *axioms* ... If no more theorems to generate, ... bastardizing the notion of an axiomatic system to the point that it ... The program was to be able to rewrite all mathematics starting using ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... It's the *axioms* ... If no more theorems to generate, ... Otherwise it's not an axiomatic system. ... The program was to be able to rewrite all mathematics starting using ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ...  It's the *axioms* ... If no more theorems to generate, ... bastardizing the notion of an axiomatic system to the point that it ... The program was to be able to rewrite all mathematics starting using ...
    (sci.logic)
  • Re: "Godel got it all wrong"
    ... that, undoubtedly, the theorems have deep philosophical meaning. ... These people are probably not really interested in technical results about recursive functions, formal theories and so forth, as pieces of mathematics, but nevertheless wish to scrutinise this or that piece of popularization, convinced as they are there's something fishy about the theorem. ... Too bad - their being messy is no reason to ignore them or pretend the answers provided by formalism of the most idiotic sort make any sense in light of the practice of mathematics. ... Formal theories are important tools in the analysis of mathematics, and certainly in some technical contexts such as axiomatic set theory where they are most of the time a purely technical tool, but for example what is important in set theory are the basic set theoretical principles, not their formalizations in the formal theory ZFC. ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... usefulness is admittedly relative to one's purposes. ... to be able to do all of the desired mathematics. ... history of set theory rather than pulling myths out of your ass. ... many proofs of theorems of Godel/Rosser/Turing et. al. ...
    (sci.logic)