Does Z assume the axiom of choice?

[Richard Botting]

Dumb question.

I've just been reading a paper that uses Z. It has a schema that declares a function f:A->B but the "where" specifies a property of f that makes it many-many. For a given a:A there can be many b:B that fit the spec. The "function" f is applied and assumed to select a particular 'b' from the many possible. This sounds like an explicit appeal to the axiom of choice...

Or I have got this wrong somehow...

[phil.c...@lineone.net]

Hi Richard,

The axiom of choice doesn't come into this.
Given
f ∈ A ⇸ B
a ∈ A
b1, b2 ∈ B
then the predicate
(a, b1) ∈ f ∧ (a, b2) ∈ f
constrains b1 and b2 to be equal. If something constrains b1 and b2 to be unequal, that contradiction would give false. Possibly the entire schema would reduce to false.

Function application in Z requires a function only at the point of application. For example,
{(0, 1), (1, 2), (1, 3)} 0 = 1
but
{(0, 1), (1, 2), (1, 3)} 1
is not defined (there is no arbitrary choice between 2 or 3). If such a situation occurs, it is possible that the author meant to use relational image, for example
{(0, 1), (1, 2), (1, 3)} ⦇ {1} ⦈ = {2, 3}

Phil

P.S. There are Z unicode characters above. Hopefully they are appearing correctly for you!

[Richard Botting]

Thanks, Phil.

The Unicode characters work well on an iMac thru Safari but not on my iPod Safari.

The axiomatic function definition attempts to say that it could be any function that satisfies the condition but doesn't give specific values. It is like wanting a function called 'dice' that maps each natural number into a number between 1 and 6. But not saying which number. Can you do this?

[Richard Botting]

I shouldn't have started this discussion without checking the history of the axiom of choice... http://en.m.wikipedia.org/wiki/Axiom_of_choice

... postulated by Zermelo and part of the ZF Set theory.

So I guess Z does assume the Axiom...