Timeline for A dual to Hilbert's $\epsilon$ operator
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 11, 2023 at 17:01 | vote | accept | Trebor | ||
| Oct 14, 2021 at 14:15 | answer | added | Noah Schweber | timeline score: 4 | |
| Oct 14, 2021 at 13:49 | history | edited | Trebor | CC BY-SA 4.0 |
added 38 characters in body
|
| Oct 14, 2021 at 13:47 | comment | added | Trebor | Yes. I'm using $\equiv$ as a meta-logical symbol. If that's the confusion I'll change it. | |
| Oct 14, 2021 at 13:42 | comment | added | Emil Jeřábek | 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. | |
| Oct 14, 2021 at 13:06 | comment | added | Trebor | See e.g. Cohen's book on the Continuum Hypothesis. | |
| Oct 14, 2021 at 13:05 | comment | added | Trebor | @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. | |
| Oct 14, 2021 at 13:01 | comment | added | Emil Jeřábek | 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)$. | |
| Oct 14, 2021 at 12:48 | comment | added | Trebor | @Emil They are equivalent as long as there are $x$ such that $P(x)$ holds. I implicitly assumed this. | |
| Oct 14, 2021 at 11:40 | review | Close votes | |||
| Oct 21, 2021 at 3:04 | |||||
| Oct 14, 2021 at 11:10 | comment | added | Emil Jeřábek | But $Q(\epsilon x.P(x))$ is not equivalent to $\forall x\,(P(x)\to Q(x))$. | |
| Oct 14, 2021 at 10:41 | history | asked | Trebor | CC BY-SA 4.0 |