Consider a formula $\forall n. \varphi $ where $\varphi$ is a 1st-order formula, over a set of $n$ variables. That is, the set of variables is determined by $n$ itself,e.g., $\forall n. \forall i. i \geq 0 \land i < n \rightarrow x_i < 10$. Is this a 2nd-order logic formula ? (as we are quantifying over all sets of variables) or is there some other logic that describes such formulas ? if it is a 2nd-order formula, what is the standard way to write it?
$\begingroup$
$\endgroup$
3
-
2$\begingroup$ Your particular formula is equivalent to asserting that $x_i < 10$ for all $i\in \mathbb{N}$. Usually, we handle this as a set of first-order formulas (called a partial type in model theory): $\{x_i<10\mid i\in \mathbb{N}\}$. Alternatively, you could treat it as a single formula in infinitary logic: $\bigwedge_{i\in \mathbb{N}} (x_i<10)$. The main point of this comment is that you don't really need to quantify over the natural numbers indexing the variables in your example. But maybe you have other, more complicated, examples in mind? $\endgroup$– Alex KruckmanCommented May 24, 2023 at 15:30
-
$\begingroup$ Probably worth noting that $\mathrm{PA}$ is happy to talk about (possible variable) finite sequences of elements, see e.g. en.wikipedia.org/wiki/G%C3%B6del_numbering_for_sequences. So if you have arithmetic and your sequences are finite, you're done. $\endgroup$– codyCommented May 24, 2023 at 20:41
-
$\begingroup$ Quantification over symbols translates into sets of formulaes (as Alex said, in model theory we use types and in logic we use infinitary logic). Generally infinitary formulaes can't be translated to second order logic (although some cases have it easy, see this interesting case) $\endgroup$– HoloCommented May 25, 2023 at 21:01
Add a comment
|