N3351 describes axioms as operations on boolean values, but it was my impression that the authors still intended the behavior similar to that of N2887, but chose not to describe it at that time. Or am I wrong?
I don't remember if we said that axioms could be evaluated (as predicates) or not. The axioms presented in n3551 are primarily intended to document the semantics; we made no serious effort to describe language features related to their interpretation. A better answer (arrived at since writing that paper) is that axioms are simply declarations of a truth about the meaning of an expression. There is work being done on language features related to this idea, but it's not mine so I won't make any effort to describe it -- I'd probably get it wrong. Andrew