Epsilon-logic is more expressive than first-order logic over finite structures (Q2710605)

The author considers the extension \(\text{FO}[\varepsilon]\) of first-order logic by means of Hilbert's \(\varepsilon\)-operator. Let \(\text{FO}[\varepsilon]_{\text{inv}}\) denote the set of \(\text{FO}[\varepsilon]\)-formulas whose semantics does not depend on the actual interpretation of the choice operator on finite structures. The author shows that there is a property of finite structures which is not \(\text{FO}\)- but \(\text{FO}[\varepsilon]_{\text{inv}}\)-definable. At the same time he shows that a similar result applies to some choice constructs considered in database theory.