I haven’t actually thought about whether A5 implies A4 though. It is plausible that it does. (together with A1-A3, or some other simple axioms,)
When A≻B, we get A4 from A5, so it suffices to replace A4 with the special case that A∼B. If A∼B, and A,B≻X, a mixture of A and B, then all we need to do is have any Y such that A≻Y≻X, then we can get Y′ between A and X by A3, and then X will also be a mixture of Y′ and B, contradicting A5, since B≻Y′.
A1,A2,A3,A5 do not imply A4 directly, because you can have the function that assigns utility 0 to a fair coin flip between two options, and utility 1 to everything else. However, I suspect when we add the right axiom to imply continuity, I think that will be sufficient to also allow us to remove A4, and only have A5.
I haven’t actually thought about whether A5 implies A4 though. It is plausible that it does. (together with A1-A3, or some other simple axioms,)
When A≻B, we get A4 from A5, so it suffices to replace A4 with the special case that A∼B. If A∼B, and A,B≻X, a mixture of A and B, then all we need to do is have any Y such that A≻Y≻X, then we can get Y′ between A and X by A3, and then X will also be a mixture of Y′ and B, contradicting A5, since B≻Y′.
A1,A2,A3,A5 do not imply A4 directly, because you can have the function that assigns utility 0 to a fair coin flip between two options, and utility 1 to everything else. However, I suspect when we add the right axiom to imply continuity, I think that will be sufficient to also allow us to remove A4, and only have A5.