Axiom of choice in CASL

[Till Mossakowski <till@Informatik.Uni-Bremen.DE>]

Dear friends,

during the development of a library for linear algebra, my colleague 
Lutz Schröder has set up a view stating that every vector space
has a basis. I could not answer the question whether this view
is defined according to the CASL semantics.

To make the point clear, let me state an easier example:

view v : 
{ sorts s,t; ops f:s->t; g:t->s; axiom forall y:t. f(g(y))=x
   hide g}
to
{ sorts s,t; op f:s->t; axiom forall y:t. exists x:s . f(x)=y }
end

On the basis of the CASL summary and the CASL semantics,
I cannot decide whether this view is legal.

The point is that the above is a legal view in CASL 
iff every surjective function has a right inverse
iff the axiom of choice is assumed in the metatheory of the CASL semantics.

I would vote for explicitly stating in the CASL semantics
(and perhaps even in the summary) that we assume the axiom of choice.

Greetings,

Till
-----------------------------------------------------------------
Till Mossakowski                Phone +49-421-218-4683, monday: +49-4252-1859
Dept. of Computer Science       Fax +49-421-218-3054
University of Bremen            till@informatik.uni-bremen.de           
P.O.Box 330440, D-28334 Bremen  http://www.informatik.uni-bremen.de/~till
-----------------------------------------------------------------------------