1
$\begingroup$

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?

Improve this question
$\endgroup$
7
  • 6
    $\begingroup$ But $Q(\epsilon x.P(x))$ is not equivalent to $\forall x\,(P(x)\to Q(x))$. $\endgroup$
    – Emil Jeřábek
    Commented Oct 14, 2021 at 11:10
  • $\begingroup$ @Emil They are equivalent as long as there are $x$ such that $P(x)$ holds. I implicitly assumed this. $\endgroup$
    – Trebor
    Commented Oct 14, 2021 at 12:48
  • 4
    $\begingroup$ No, they are not. Take already the simplest case when $P(x)$ is just $\top$. Then $\epsilon x.\top$ is just an unconstrained new constant $c$. For general $Q$, it is certainly not the case that $Q(c)$ is equivalent to $\forall x.Q(x)$, or to any other formula not containing $c$ for that matter. The only things you know about $Q(\epsilon x.\top)$ are that it obeys the implications $\forall x\,Q(x)\to Q(\epsilon x.\top)$ and $Q(\epsilon x.\top)\to\exists x\,Q(x)$. $\endgroup$
    – Emil Jeřábek
    Commented Oct 14, 2021 at 13:01
  • $\begingroup$ @Emil Why doesn't $Q(c)$ for an unconstrained constant $c$ mean $\forall x. Q(x)$? It is an inference rule in the formulation of first order logic I'm using. $\endgroup$
    – Trebor
    Commented Oct 14, 2021 at 13:05
  • 3
    $\begingroup$ That’s a variant of the generalization rule, yes. But it does not make $Q(c)$ and $\forall x\,Q(x)$ equivalent; it only states that one is derivable if and only if the other one is derivable, in a theory that does not otherwise include the $c$ constant. $\endgroup$
    – Emil Jeřábek
    Commented Oct 14, 2021 at 13:42

1 Answer 1

Reset to default
4
$\begingroup$

Nothing like this can happen.

Take $P(x)\equiv\top$, and let $S$ be any formula such that both $\exists x S(x)$ and $\exists x\neg\ S(x)$ are derivable. Then both $$(*)_1:\quad\exists x(P(x)\wedge S(x))$$ and $$(*)_2:\quad \exists x(P(x)\wedge\neg S(x))$$ are themselves derivable. However, we can't possibly have a single term (or term-like piece of syntax) $\delta$ such that $Q(\delta)$ is equiderivable with $\exists x(P(x)\wedge Q(x))$ for either choice of $Q\in\{S,\neg S\}$: each sentence of the latter type is outright derivable, while since $\delta$ is independent of $Q$ we can't have both $S(\delta)$ and $\neg S(\delta)$ be derivable.

For a concrete example, what should your $\delta$ do in the setting of the natural numbers and first-order Peano arithmetic when we take $P(x)\equiv\top$ and $Q(x)\equiv$ "$x$ is even"?

Improve this answer
$\endgroup$
3
  • $\begingroup$ Yes, that matches up with my intuition. The motivation for this is to provide a more formal account for the big-O notation. Adding such a construct seems to require a substantial change of the formal system, e.g. treating $\delta$ as a special symbol, which is far less natural than the introduction of $\epsilon$. $\endgroup$
    – Trebor
    Commented Oct 14, 2021 at 14:20
  • $\begingroup$ @Trebor This is perhaps a tangent, but: what do you see as informal about the usual definition of big-O, and why would formalizing it require us to change our underlying logical formalism? $\endgroup$
    – Alex Kruckman
    Commented Oct 14, 2021 at 15:33
  • $\begingroup$ @AlexKruckman Well, certainly the use of equality in the context of big-O is [unprintable sound effect], so I do have some stylistic sympathies. :P $\endgroup$
    – Noah Schweber
    Commented Oct 14, 2021 at 15:37

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .