Skip to main content
2 of 2
added 38 characters in body
Trebor
  • 1.3k
  • 6
  • 16

A dual to Hilbert's $\epsilon$ operator

Hilbert introduced a construct $\epsilon x. P(x)$ for a predicate $P$ such that $$\exists x. P(x) \implies P(\epsilon y.P(y))$$

Obviously, this is equivalent to the axiom of global choice. With this operator, we can form complex propositions conveniently:

$$Q(\epsilon x. P(x)) \text{ equiderivable to } \forall x. P(x)\implies Q(x)$$

assuming $\exists x. P(x)$. I'm wondering if the dual can be achieved. I.e. Can there be an operator $\delta x. P(x)$ such that

$$Q(\delta x. P(x)) \text{ equiderivable to } \exists x. P(x)\land Q(x)$$

I suspect that the difficulty encountered in defining this is because we implicitly assume universal closure, but not existential closure. Is there any material related to this?

Trebor
  • 1.3k
  • 6
  • 16