Groups | Search | Server Info | Login | Register

Groups > comp.specification.z > #392

Re: Does Z assume the axiom of choice?

Show all headers | View raw

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!

On Wednesday, 28 January 2015 19:33:44 UTC, Richard Botting  wrote:
> 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...

Back to comp.specification.z | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

Does Z assume the axiom of choice? Richard Botting <rjbotting03@gmail.com> - 2015-01-28 11:33 -0800
  Re: Does Z assume the axiom of choice? phil.clayton@lineone.net - 2015-02-01 23:53 -0800
    Re: Does Z assume the axiom of choice? Richard Botting <rjbotting03@gmail.com> - 2015-02-02 10:54 -0800
      Re: Does Z assume the axiom of choice? Richard Botting <rjbotting03@gmail.com> - 2015-02-03 15:10 -0800

csiph-web