I'm glad to see this discussion.
I believe that N3351 is not a good place to learn axioms from.
It's a reasonable place to start as long as you don't expect too much from them. The axioms presented in that paper were primarily intended to document the semantics of a type; we had not planned (at that time) any particular ideas about how they should or could be used by the compiler.
(2). Axioms need not hold for all values of the given type, but only for those values that a given algorithm (constrained by a concept with axioms), and only in expressions that are really stated in the executed algorithm.
Axioms, in the context of a concept, are intended to hold for all values of type. A precondition is a property of specific values or objects and is not an axiom.
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*. Andrew