For instance, axiom EqualityComparable::Reflexivity states that some (rather than every) objects must compare equal to themselves. If you consider type float, objects with value NaN (not-a-number) compare unequal.
No; all well-formed values of a type can be compared for equality (if the type is EqualityComparable). NaN is not a well-formed value. It is literally *not a number*.
Unless you mean to say that any program that uses a NaN in any way has undefined behavior, this notion of a "well-formed value" seems arbitrary and capricious.
This entry at Bjarne Stroustrup's FAQ: http://www.stroustrup.com/C++11FAQ.html#axioms presents a reasonable "semantics" of axioms. If an axiom states an equivalence between two expressions, compilers and other tools are allowed to make an assumption that one expression can be substituted for another and perform optimizations or other code transformation or analysis based on this assumption regardless if the assumption holds or not. When you instantiate template FUN with type X, you are responsible for guaranteeeing that this assumption will hold. Under this interpretation we do not care (while doing transformations) that we get NaN or not. In fact, the following axiom: x / y * y <=> x; could be used to avoid the generation of NaN value for some values of x and y. Of course, such "allowance of substitution" would only make sense inside concept-constrained function templates (or member functions of class templates) because in "free code" (i.e, with no templates, you may want to rely on the semantics of NaN's.Also, with the previous concept design that used concept maps, a type could model some concept in more than one way. For instance type int models concept Monoid in two ways: using addition and identity element 0 as well as using multiplication and element 1. I am not sure how the making use of axiom would work in such situations unless we are in a constrained template. Regards, &rzej