Skolem in his (1928) is credited (cf. Van Heijenoort, 1967) with a decidability proof for FOL formulas of prefix $\forall x\exists y_1,...,y_m $.
Let $U = \forall x\exists y_1,...,y_m F $. For formulae of this class, Skolem shows how his procedure $\mathcal{R}$ constitutes a decision procedure for a basic alternative: either for some $n$, there are no solutions to the $nth$ level approximation of $U$, or, there are solutions for approximating arbitrarily high $n$. (“Solutions” are truth-value assignments to conjunctions of instances of $F$ that approximate to $U$ - see https://mathoverflow.net/q/373381/116705 for background).
What makes the decision problem tractable for formulas of prefix $\forall x\exists y_1,...,y_m $ is that contradictions can only arise between approximations of consecutive levels. This is because each argument sequence of level $n$ ($n>0$) will have only a single element in common with the argument sequences of level $n-1$, and no elements in common with levels below $n-1$.
For this reason it suffices to look for the first level $n$ at which solutions starting from level 0 can be consistently extended to the next level. The pattern of consistency between the solutions at levels $n$ and $n+1$ will then hold for any level $m>n$, guaranteeing the possibility of extending solutions to the next level for arbitrarily high levels, and ruling out the possibility of encountering a level higher up where all the paths from level 0 terminate.
The existence of such a level can be decided in finite time. All paths through the tree of solutions must start from one of finitely-many solutions of level 0. These solutions are progressively narrowed down as the paths terminate at higher levels. The method either eliminates all level 0 solutions, reaching a level after which none of the level 0 solutions can be extended, or, it reaches the level $n$ described above where all the level 0 solutions with extensions through the $nth$ level can be consistently extended through the $n+1th$ level. In the former case, the formula is unsatisfiable; in the latter, it has solutions for arbitrarily high $n$.
To get from here to decidability presumably uses a result Skolem proved in 1922. There Skolem shows how, from the existence of solutions for every n, one can construct a solution to the original quantified formula in the domain of natural numbers (one version of the Lowenheim-Skolem theorem).
Of course, the hypothesis of the 1922 result is not that the formula "has solutions for arbitrarily high $n$" but that it has solutions for every n. And yet Skolem's decision procedure seems to guarantee only solutions for arbitrarily high $n$. This does not fulfill the conditions to apply the 1922 theorem in order to prove satisfiability.
Question: Is there a finitistic alternative to the Lowenheim-Skolem theorem that could be used to secure the result Skolem wants in this case, namely, the decidiability of satisfiability, based on the decision procedure described above?
References:
Skolem, Thoralf. [1928] On Mathematical Logic. English translation in van Heijenoort (ed.) [1967], pp. 508– 524.
VAN HEIJENOORT, JEAN (ED.) [1967b] From Frege to Gödel; a source book in mathematical logic, 1879-1931. Cambridge, Harvard University Press.