Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: logic

Topic: Bounded quantification over postulated sets

Nikolaj Kuntner (Mar 16 2023 at 23:56):

In something like plain ZF, and in particular without extending the language, if $P(x)$ is a $\Delta_0$-formula, is
$\forall(x\in\omega). P(x)$,
(short for $\forall x. (x\in\omega)\to P(x)$) also a $\Delta_0$-formula?
And if so, how's it justified? I mean even if "$\omega$" can be specified by a $\Delta_0$-formula formula $\mathrm{FirstInf}(w)$, and also if "$x\in\omega$" is provably equivalent to a $\Delta_0$-formula $\mathrm{FinNum}(x)$ in the theory, then I still only get a rewriting of the proposition in the form $\forall w. \mathrm{FirstInf}(w)\to \forall(x\in w). P(x)$ resp. $\forall x. \mathrm{FinNum}(x)\to P(x)$, which are not technically of a bounded form.
If there's no rewriting that makes it evident, maybe one can speak in terms of parameters ("$\forall(x\in\omega). P(x)$" with $\omega$ denoting a mere set parameter is $\Delta_0$). But for systems like MacLane's or Kripke–Platek set theory, where the classification is relevant, this seems to make the book-keeping of the proof calculus complicated. I come to the question because I think arithmetical formulas with quantifiers over the naturals are considered $\Delta_0$ in the set theory model context. Generally, if I express an only arithmetical statement with quantifiers in set theory in full, I must account for $\omega$ one way or the other.