Re: grassroots level SPARK Initiation

[Paul Rubin <no.email@nospam.invalid>]

Mehdi Saada <00120260a@gmail.com> writes:
>> Most math is fundamentally about reasoning about infinite sets. 
> Except men have been doing math way before last century's mania with
> set theory.

Yes, usually with the integers (of which there are infinitely many) or
else with geometry (lines, planes, or space of infinite size).  Set
theory itself is much more recent of course.  I don't think it's really
come up in this discussion except in saying math is about infinite sets,
but if you prefer, we could say infinite structures (again the classic
example is the integers).

> The computer is *never* counting up to the infinite, of
> course... It's not *reasoning* about infinite stuff either, it's
> always applying a logical, step-by-step recipe, however complex.

We're talking about SPARK whose purpose is to prove theorems about
programs (that they don't crash, etc).  Yes, proving theorems is reasoning.

> see NJ.Wildberger, math teacher on YT ... Just be sure this stance
> isn't coming from nowhere, nor is devoid of reason.

OK, I looked at a couple minutes of video and some of the articles on
his web site, and he seems to be espousing some views in the philosophy
of mathematics connected with an idea called finitism.  That's a little
bit off the beaten path, but some good mathematicians such as Edward
Nelson have worked in that area.  But if you look at

  http://web.maths.unsw.edu.au/~norman/papers/Ordinals.pdf

it's very clear that Wildberger understands the conventional approach
perfectly well, so you should learn it too.  Also I think he objects to
completed infinities (like the ones in set theory) but seems ok with
potential infinities (like the integers under the first-order arithmetic
axioms).  Not allowing completed infinities means we can't collect the
integers into a single object, but there is still no largest integer,
and we can quantify over the integers to say "every integer has a
successor" and things like that.

Anyway Enderton's book on logic might mention set theory in a place or
two, but it's not really an important part iirc.  (He has a separate
book on set theory which you might not went to read).  You won't
encounter set theory much in computer science.  In fact the logic used
in software proofs is usually intuitionistic logic (aka constructive
logic).  Not that there's anything wrong with classical logic, but
intuitionistic logic happens to work better for the results you want.

> I'll look at it. Do you know "HOW TO PROVE IT, A Structured Approach",
> from Daniel J. Velleman ? It's lengthier, among other things.

It looks like a nice book about doing math proofs, so you should
certaintly study it if the stuff in it isn't familiar to you.  But it's
not a logic book.  It might be reasonable to put logic aside temporarily
and read Velleman's book first.