Nonconstructive reasoning in Skolem's proof of the Löwenheim-Skolem Theorem

Question

I am trying to understand where nonconstructive reasoning occurs in this passage from Skolem’s (1922) proof of the Löwenheim-Skolem theorem. As background, Skolem’s “solutions” are assignments of truth-values to the atomic components of a propositional formula U, and each step considers progressively more instances of U, as part of the process of constructing a model of U’s quantified counterpart F. The ordering is such that $L \leq L'$ if the first atomic component of U on which they differ gets assigned FALSE in $L$ and TRUE in $L'$:

Let $L_{1,n},L_{2,n},...,L_{e_n,n}$ be the solutions of the nth step. If we now form the sequence $L_{1,1},L_{1,2},...$ of the first solutions, we can verify without difficulty that they converge in the logical sense. For let $L_{1,n}$ be a continuation of $L_{{a_v^n}_v}$ $(n> v)$. Then, if $n'> n$, ${a_v^n}_v$ ≦ ${a_v^{n'}}_v$ . But, since the number ${a_v^n}_v$ can only have values 1 to $e_v$ it must remain constant for all sufficiently large $n$. Thus we can obtain as "limit" the fact that the first-order proposition is satisfied in the domain of the entire number sequence, q.e.d. (Skolem 1922, p. 294 in From Frege to Godel, van Heijenoort, 1967)

The proof is alleged (Brady, 2000) to make implicit appeal to the Bolzano-Weierstrass theorem that every infinite subset S of the closed interval [a, b] of real numbers contains a convergent infinite sequence.

The use of nonconstructive reasoning in the proof of the B-W theorem is clear. The convergent sequence is defined inductively by:

(1) If $[a_n,(a_n + b_n)/2]$ contains infinitely many elements, let $a_n+1 = a_n$ and $b_n+1 = (a_n + b_n)/2$

(2) If $[a_n,(a_n + b_n)/2]$ contains finitely many elements, let $a_n+1 = (a_n + b_n)/2$ and $b_n+1 = b_n$.

The law of excluded middle is here applied to the infinite set of intervals to guarantee that either (1) or (2) holds in every case.

Skolem's proof also looks to be defining a sequence by choosing at each level v a solution $L_{{a_v^n}_v}$ that is extended by infinitely many higher-level solutions (this is how I interpret the significance that ${a_v^n}_v$ "remains constant" for large $n$.)

But rather than assume (by LEM) that for every solution L, the set of solutions extending L is either infinite or it is finite (even though there may be no effective way of deciding which), Skolem's proof seems to actually specify the desired $L_{{a_v^n}_v}$: it is the least solution in the ordering defined above that agrees with infinitely-many solutions on their assignment up to the vth level.

My question is: has Skolem avoided the nonconstructive appeal to LEM by explicitly defining an ordering on the (finitely-many) solutions at each level? If so, where else is nonconstructive reasoning being smuggled in?

Answer 1

If I understand the proof correctly, it uses the following fact:

Statement: A monotone sequence $b : \mathbb{N} \to \{0,1\}$ stabilizes, i.e., there is $d \in \{0, 1\}$ and $n$ such that $b_m = d$ for all $m \geq n$.

This statement is not constructively provable because it implies LPO. Indeed, given $f : \mathbb{N} \to \{0,1\}$, consider the sequence $b_n = \max(f(0), \ldots, f(n))$. It is monotone, so by the above statement it stabilizes. If it stabilizes at $0$ then $\forall n . f(n) = 0$, and if it stabilizes at $1$ then $\exists n . f(n) = 1$.