Thanks Waldek. I don't really have a problem with providing a value for x/0. This is not so different than considering the CardinalNumber domain as an extension of NonNegativeInteger. CardinalNumber is not used much in FriCAS except as the domain of the operation 'dimension' (of VectorSpace, etc.) however it includes a value of Aleph(0) for infinite cardinality. I suppose that it would be possible to define something like this for Float, e.g.
x/0 = Aleph(1) and we have x ~= Aleph(1) for all values in Float except Aleph(1). But I worry if the proposal really is that x/0 = 0 since that could do a lot of damage to many other desirable properties that Float has Field should imply, e.g. as Bertfried pointed out concerning it's topological properties. I agree that FriCAS (and mathematics in general) needs a stronger more general logic. In fact isn't "higher order logic" the main point of Isabelle/HOL? Therefore I do not understand why Jalaluddin Morris claims that Isabelle/HOL somehow legitimizes this choice for the "field of real numbers". Regards, Bill Page. On Thu, Mar 24, 2011 at 5:51 PM, Waldek Hebisch wrote: > > Well, x/0 = 0 is pretty standard in logic: in logic one wants > total functions so _some_ definition of x/0 is required. Then > using 0 as a value is most natural. If you want to stay in > the "most classical logic", that is first order logic with > total functions, then FriCAS field is not a legitimate mathematical > structure, becase in FriCAS division is a partial function > (so for FriCAS you need "stronger" logic). > > The intent of this definition is that you really do not want to > compute things like 1/0, but for formal reasons you can not avoid > them. Consider: > > (x ~= 0) and (z = 1/x) > > This is a fine, sensible logical formula: when 'x' is 0 then the > formula is false due to first term and if 'x' is different from 0, > then division is well-defined. But if 'and' is a function and > we evaluate arguments first we may be forced to compute '1/0', > use it in comparison and then effectively throw out the result > of the comparison. > > Of course, if one really makes use of exact value of x/0 then > it is confusing... > -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en.
