In the 1920s, the Entscheidungsproblem or decision problem was a key area of investigation. This is the question of whether the satisfiable formulas of first order logic (or some fragment thereof) were decidable. At the time, a solution to this problem meant the discovery of a finitely executable method to determine, for a given formula F, whether F had any models (was satisfiable) or whether F had no models.
One approach to a solution was via the methods used by Lowenheim in 1915 to prove the Lowenheim-Skolem theorem. Lowenheim, and later, Skolem, proved this theorem by constructing a leveled sequence of instances which approximate to the quantified formula. The corresponding ``solutions'' to these instances taken together yield a model in the limit, by a step equivalent to Konig's infinity lemma. In this way, Lowenheim and Skolem show that:
If a formula F has solutions of level $n$ for all $n$, then F is satisfiable in the domain of natural numbers.
This method also yielded a decision procedure for some classes of FOL formulas - those with a certain quantifier prefix. The method would ultimately prove inadequate to provide a decision procedure for all of FOL in light of Church's undecidability theorem.
However, the method could still yield a lesser result, a semi-decision procedure for unsatisfiability/validity:
(SD) For some $n$, F does not have solutions of level $n$ if and only if F is unsatisfiable.
By searching through the levels, we are guaranteed to find a finite level with no solution, provided F is unsatisfiable. If F is unsatisfiable then its negation ~F is valid.
One to prove the hard (<-) direction of (SD) is to via the contrapositive of the Lowenheim-Skolem theorem: If F is unsatisfiable, then it is not the case that it has solutions for every $n$.
This does not give us any information about which $n$ has no solutions, but it does guarantee - non-constructively - the existence of such a $n$.
Questions:
(1) From a modern perspective, apart from the lack of info about which $n$, does the non-constructivity of this proof impugn the resulting semi-decision procedure in some way?
(2) From a historical perspective, could the lack of a clear metatheory versus object theory distinction lead a (pre-1930) logician to think that the resources for proving a decidability result had to also be ``effective'' or at least constructive?