The Logic of Choice
Andreas R. Blass, Yuri G. Gurevich · Journal of Symbolic Logic · 2000
Abstract The choice construct (choosex: φ(x)) is useful in software specifications. We study extensions of first-order logic with the choice construct. We prove some results about Hilbert'sεoperator, but in the main part of the paper we consider the case when all choices are independent.