Zero breaks the postconditions of division. So?
Not always. Dividing by 0.0 for floating point types is a valid operation resulting in inf. But that only applies to a IEEE floating point types. Perform the same computation with rational number and you might get an assertion or exception. But you might not. It depends on your choice of implementation. One of the goals of looking at semantics in this way is to help programmers document and better characterize the requirements of their algorithms. An algorithm that computes generically over Fields necessarily excludes NaN as an input and must guard against division by 0. An algorithm that computes over, say, ExtendedReals may allow division by 0, but also excludes NaN. A generic algorithm designed specifically for floating point types allows division by 0 and NaN as inputs. The point isn't to change the meaning of existing programs by excluding certain values or expressions. Axioms should present a consistent logical framework that precisely but generally describe the semantics our existing programs. This is not easily done.