[FOM] Intermediate value theorem and Euclid

[Vaughan Pratt]

On 5/21/2009 5:37 PM, Andre.Rodin at ens.fr wrote:
> Vaughan Pratt wrote:
>
>> Is there *the right* notion of abelian group?  If not, why not?  If so,
>> why that and not *the right* notion of Euclidean plane?
>
> I think that NOT. Let's just talk about *group* (if I am right about *group* the
> same holds for *abelian group*). Of course the group concept can look very
> different: its today's standard presentation as a set with a binary operation
> subject to the axioms is a more recent invention that the notion of group
> itself. And there is today an alternative definition of group around: as a
> category with exactly one objects and all morphisms reversible.

Oh, ok, you're using "notion" synonymously with "presentation" or 
"definition."  Yes, I have no difficulty with multiple presentations or 
definitions of "the same thing."

However for me the "notion" of a concept is the common element of its 
different presentations when there is a consensus that they are 
equivalent up to a mutually agreed-on level of detail.

So now that we've established that we have different notions of 
"notion," you have me worried that maybe I'm using the term 
nonstandardly.  What do other people mean by "the notion of integer" or 
"the notion of a topological space?"  Would you consider glaringly 
different yet demonstrably equivalent definitions of "topological space" 
to be different notions thereof or different definitions of the same notion?

If I'm simply off base here (as often the case) then I'll start using 
"notion" more standardly.  If however there is no consensus then perhaps 
the word "notion" should be avoided when talking about the foundations 
of mathematics to avoid talking at cross purposes.

> But anyway Euler didn't think about
> the affine space as we usually do this today, he didn't have in mind our notion
> of affine space as a set with a structure

Indeed, or for that matter as a *space* with structure---why should a 
structured object need an underlying set when equational logic 
(organized as a monad) can furnish the objects of other categories than 
Set with structure?

You're probably right that Euler didn't have any operations on affine 
space in mind, though it's a very natural thing to have, even without 
any conception of coordinates or vector addition.  For example the facts 
that in affine space one can retrace one's steps exactly without 
changing gait, and that stepping in place takes one nowhere, reflect 
structural properties of affine space.  And there are others that even 
Euclid could have exploited had he formulated his five postulates a 
little more constructively to go with the constructive nature of his 
proofs (the drift of my FMCS'09 talk at UBC on May 31).

If the constructs assumed by the proofs of Book I of Euclid, when 
expressed as operations, turned out to be just another basis for the 
linear and bilinear operations of the standard two-dimensional real 
inner product space, we could then say that Euclid had the modern 
"notion" (or whatever the correct term is) of the Euclidean plane in the 
same sense that Boolean lattices and Boolean rings are just different 
bases for the same notion of Boolean algebra.

Vaughan Pratt