An investigation concerning the Hilbert-Sierpiński logical form of the axiom of choice.
Charles “Chuck” Davis · Notre Dame Journal of Formal Logic · 1975
in fact equivalent to the axiom of choice in the field of logic, it will be referred to as the Hubert-Sierpiήski logical form of the axiom of choice.In [9], Hubert introduced the ε-calculus 1 which ''differs from the ordinary first-order functional calculus by not containing quantifiers among the primitive notation'' ([3], p. 183), as a part of the finitistic examination of the foundations of mathematics.By introducing a new primitive term, ε, by means of the axiom schema:Hubert was able to define the particular quantifier by:and prove all the usual rules of quantification theory ([10], pp.67-68).The intuitive reading of ( ε x F(x)' is 'an F', or more concretely, ( ε x (x is a man)' is read 'a man'.Thus 'ε' corresponds, more or less, to the indefinite article 'a' ('an'), and A is to be read "If anything has the property F, then an F has the property F".Although Hubert seems to see a connection between A and the axiom of choice, in that he refers to the ε-operator as playing the role of a choice function ([10], p. 68), others find it misleading to refer to A as a "generalized principle of choice". 2 Wang argues that:If the axiom of choice were a special case of the ε-rule, why does the consistency of the axiom of choice not follow from the ε-theorems according to which application of the ε-rules can be dispensed with if the ε-operator occurs in neither the axioms nor the conclusions?Indeed, if the axiom of choice were derivable from the ε-rule, we would, by the ε-theorems, be able to derive the axiom of choice from the other axioms of set theory. 2 In [23], Sierpiήski states what he calls Hubert's axiom:B There is a function, ε, associating with every property, P, for which there exists at least one object having that property, an object, ε(P), having the property P. and argues that "From the logical axiom ... it follows that there exists a function associating with every non-empty set a certain element of that set".Sierpiήski carries out the proof by associating with every set, A, the property of being an element of A, P A .Substitution of ζ P A 9 for 'P' in B, gives:C There is a function, ε, associating with each non-empty set, A, an element of that set ε(P A ) Sierpiήski goes on to show that in the field of set theory C is inferentially equivalent to the axiom of choice. 3 At first glance it would seem that Wang and Sierpiήski are in disagreement, however, it disappears on closer examination.What Sierpiήski calls Hubert's Axiom is in fact not an accurate rendering of A. Rather, it is an informal version of: