Can FOL include infinite disjunctions?

Question

There are several posts on Math S.E. which claim that first order logic (FOL) can not include infinite disjunctions, but so far there are no proofs of the fact.

How can I prove that infinite disjunctions can not be included in FOL?

This is a self answer question.

References:

1. Infinite Disjunctions and Conjunctions
2. First-order Logic with infinite conjunction
3. Why does the compactness theorem not apply to infinite languages?
4. Infinitely long formulas (This one points out that FOL formulas are defined to be finite, but it does not show that there is no way to extend the definition to include infinite ones).
5. Are quantifiers only required because of infinite proposition chains?

Answer 1

The reason that first-order logic does not allow infinite disjunctions is simply by definition. No infinite formulas are allowed, so in particular no infinite disjunctions. However, we could still ask if it is possible for a formula $\varphi$ to be equivalent to an infinite disjunction $\bigvee_{i \in I} \psi_i$. By compactness this can only be the case if there is a finite subset $\{i_1, \ldots, i_n\} \subseteq I$ such that $\varphi$ is equivalent to the finite subdisjunction $\psi_{i_1} \vee \ldots \vee \psi_{i_n}$.

To see this: consider the set $\{\varphi \} \cup \{\neg \psi_i : i \in I\}$. This is inconsistent, so by compactness there is a finite subset that is inconsistent. So we find $\{i_1, \ldots, i_n\} \subseteq I$ such that $\{\varphi, \neg \psi_{i_1}, \ldots, \neg \psi_{i_n}\}$ is inconsistent. So we get that $\varphi$ implies $\psi_{i_1} \vee \ldots \vee \psi_{i_n}$. The converse is trivial.

---

In your question you also mention "extend the definition to include infinite [formulas]". This is in itself no problem, and gets us into the realm of infinitary logic. The problem is that we lose many useful tools that we have in first-order logic, like the compactness theorem (as the above demonstrates).

It is worth mentioning that in model theory we often consider what are effectively infinite conjunctions. These are called types: a type is a (possibly infinite) consistent set of formulas. Of course, satisfying an entire set of formulas is the same as satisfying the infinite conjunction of those formulas (and it does thus not break compactness).

Answer 2

Suppose that an infinitely long disjunction (1) exists.

\begin{equation}\tag{1}a_1\lor a_2\lor a_3\lor\dots\end{equation}

Then consider an infinite collection of formulae (2), consisting of the negation of each instance of the disjunction.

\begin{equation}\tag{2}\{\lnot a_1,\lnot a_2,\lnot a_3,\dots\}\end{equation}

A theory $T$ consisting of (1) and all the formulae in (2) will necessarily be unsatisfiable, as each negated propositional atom $a_i$, cannot be satisfied unless the atom is false, which implies that the infinite disjunction is false.

However, every finite subset of formulae in $T$ will be satisfiable, (e.g. $\lnot a_1\land(a_1\lor a_2\lor a_3\lor\dots)$), so by compactness, the set comprising all formulae in the theory will be satisfiable.

This is a contradiction, so it is not the case that an infinite disjunction is permitted in FOL.