Does compiler have the authority (from formal point of view of C++ axioms) to stop compilation with error in such case(of course, if it able to diagnose that)?
I believe it should, but I do not know the mechanism that it should use to diagnose the error.
If compiler has right to reject wrong axioms when he able to diagnose, then we can't use C++ axioms to express in code our assumption about floating-point addition associativity.
Whatever mechanism is eventually designed to check axioms would have to accommodate floating point issues. This is an area of active investigation. What you had in n3351 and 2887 were initial attempts to say, in general, what was desired, but not exactly how it should work. In n3351, we didn't know what we wanted the compiler to do with axioms; describing language mechanics wasn't the primary focus of that work. In n2887, the authors had a better idea of what they wanted, but didn't (if I'm recalling correctly) specify the mechanics of how they could be checked.
So, I am confused about real intention.
The intent is to state requirements. Translating that to a working language specification is a work in progress. Andrew