What logic can express this sentence?

Question

Trying to figure out the logic in which the following formula is expressible: $\forall i\in N: (x_i > y_i)$, which is equivalent to the "infinite" conjunction $\bigwedge_{i\in N} (x_i > y_i)$.

Now a 1st order logic allows arbitrary number of variables $\{x_i,y_i\mid i\in N\}$, but only a finite number of atomic formulas can be composed. (Here $x_i > y_i$ is an atomic formula based on binary predicate "$>$", and so the above formula is a composition of infinite number of atomic formulas.) Thus in the form written, the above doesn't seem to be a formula of 1st-order logic. Also, it's not clear how to rewrite this formula in 1st-order logic if indeed it belongs there.

Next in 2nd-order logic, that allows quantification over predicates (as well as functions), again it is not clear whether the above can be written as formula in 2nd-order logic.

Any insights? Thanks.

Answer 1

You're looking for infinitary logic - probably $\mathcal{L}_{\omega_1\omega_1}$ if you're using countably many distinct free varables. See https://en.wikipedia.org/wiki/Infinitary_logic, as well as https://www.math.wisc.edu/~keisler/kk2.pdf (the latter is a biographical paper about Barwise, but it is also a good source on infinitary logic in general).

---

Basically, here's how it works: we fix cardinals $\kappa$ and $\lambda$, with $\kappa\ge\lambda$. Then $\mathcal{L}_{\kappa\lambda}$ is (informally) the set of formulas generated by starting with first-order logic and closing under

• conjunctions and disjunctions over sets of $<\kappa$-many formulas, and

• quantification over $<\lambda$-many variables.

We can also define proper class sized infinitary logics as $$\mathcal{L}_{\infty\lambda}=\bigcup_{\kappa\in Card} \mathcal{L}_{\kappa\lambda}\quad\mbox{and}\quad \mathcal{L}_{\infty\infty}=\bigcup_{\lambda\in Card}\mathcal{L}_{\infty\lambda}.$$

Of course, the precise definitions are a bit technical, but this is the key idea.

Of special interest is $\mathcal{L}_{\infty\omega}$, which is roughly the "logic of back-and-forth arguments": two structures are $\mathcal{L}_{\infty\omega}$-equivalent iff player II has a winning strategy in the Ehrenfeucht-Fraisse game of length $\omega$ - or, equivalently, if there is some forcing extension of the universe in which they become isomorphic. (The first fact is due to Karp; the second is folklore, but I believe first observed by Barwise.)

---

Note that we could similarly define infinitary second-order logic, etc. I know less about such things, though.

Answer 2

Using infinitary logic to express your statement is somewhat overkill. The usual formulation of 2nd order logic only allows subsets $X\subseteq\mathbb{N}$ to be quantified over (which can be seen as functions $X\rightarrow {\bf 2}$) rather than arbitrary functions, which would easily allow you to define two sequences $x,y:\mathbb{N}\rightarrow\mathbb{R}$ and say $$ \forall i\in\mathbb{N},\ x(i)>y(i)$$ as mentioned in the comments.

However, the usual formulation of 2nd order logic is quite strong, and functions $\mathbb{N}\rightarrow\mathbb{N}$ and sequences $\mathbb{N}\rightarrow\mathbb{R}$ can easily be coded in it! I'll try to sketch the argument below, but first note that because of all this expressive power, there's no hope of quantifier elimination or decidability in this logic.

1. Coding rationals: first note that by usual arithmetic tricks that I won't get into here, it's easy to code pairs in $\mathbb{N}\times\mathbb{N}$, triples etc. even finite sequences using just natural numbers. By suitably defining operations and equality, we can code $\mathbb{Z}$ as a subset of $\mathbb{N}\times\mathbb{N}$, and $\mathbb{Q}\subset \mathbb{N}\times \mathbb{Z}$, so $\mathbb{Q}$ is coded as a subset of triples, themselves coded as natural numbers.

2. Building real numbers. So by 1. to build a function $\mathbb{N}\rightarrow \mathbb{Q}$, it suffices to build functions $\mathbb{N}\rightarrow \mathbb{N}$! But this can be done by describing a function $f$ as a subset $f\subseteq\mathbb{N}\times\mathbb{N}$ with certain properties, as is done in set theory. As before, pairs can be coded as individual numbers, so you can describe these subsets in 2nd order arithmetic.

3. Now that real numbers are described as sequences of natural numbers (elements of $\mathbb{N}\rightarrow\mathbb{N}$, it's pretty easy to build sequences of real numbers, by noticing that a function $f:\mathbb{N}\rightarrow \mathbb{N}^{\mathbb{N}}$ is just a function $\hat{f}:\mathbb{N}\rightarrow\mathbb{N}\times\mathbb{N}$ (known as the reverse curryfication of $f$, or as Schönfinkel's trick).

---

To answer your follow-up question, I don't know of any quantifier elimination for ${\cal L}_{\omega_1\omega_1}$, but keep in mind that even quantifier-free formulas are undecidable in that logic, because of it's infinitary nature (which makes it not very interesting, in my opinion).