Hilbert's \(\varepsilon{}\)-operator and classical logic (Q1208146)

In the framework of the first-order language the \(\varepsilon\)-axiom corresponding to the famous Hilbert's \(\varepsilon\)-operator can be formulated as follows: \(A(x)\to A(\varepsilon_ A)\), where \(A(t)\) is obtained as the result of substituting term \(t\) for each free occurrence of \(x\) in \(A(x)\). Namely, \(\varepsilon_ A\) can be considered as an ideal object associated with \(A\) such that all one knows about it is that, if anything satisfies \(A\), it does. Logical relationships of the \(\varepsilon\)-axiom with some basic superintuitionistic axioms are analyzed and the roles of the extensionality principle and principle of bivalence are discussed. An algebraic type semantics for the extension of the Heyting first-order predicate calculus by the \(\varepsilon\)-axiom is described with the corresponding soundness theorem, but the provision of a complete semantics for this calculus remains an open problem.