In his (1928), Skolem describes a decision procedure for first order formulas with the prefix $\forall \exists$. We can think of Skolem’s procedure as a sort of infinite truth table, where at each level we assign truth values to approximating instances of the quantified formula. The construction of approximations is described here. As we ascend in level, we progressively narrow down the finitely-many truth assignments according to whether they have extensions at higher levels. We demonstrate this procedure for one of Skolem’s example formulas (p. 520 of 1928). Question follows below.
Let U = $\forall x \exists y [[ A(x,y) \land B(x) \land \neg B(y)] \lor [A(x,x) \land \neg A(y,y) \land \neg B(y)]]$.
The first step is to drop the quantifiers.
The first level consists of all possible truth assignments to atomic components that make the 1st level instance of the formula (without quantifiers) come out true. This is the instance where we instantiate $x$ by 0 and $y$ by 1.
$[A(0,1) \land B(0) \land \neg B(1)] \lor [A(0,0) \land \neg A(1,1) \land \neg B(2)]$
These ``solutions’’ are represented by rows $a_1 - g_1$ in the following chart.
At the second step we rule out the 1st level solutions represented by rows $a_1, c_1, e_1, f_1$, and $g_1$ . These are not compatible with any 2nd level solution because no 2nd level solution makes both A(1,1) and B(1) false. (Note that when checking for consistency we can disregard the first column for the atomic formula A(x,y) since potential contradiction between levels can only occur with the formulas B(x) and B(y) and A(x,x,) and A(y,y).) The solutions $b_1$ and $d_1$ however are compatible with some 2nd level solutions, specifically, those in rows $d_2$ and $f_2$.
Restricting our attention to these 2nd level solutions that extend $b_1$ or $d_1$, we now ask whether any of these have extensions of the 3rd level. Since both $d_2$ and $f_2$ assign False to A(2,2), this rules out all but two of the 3rd level solutions (rows $d_3$ and $e_3$).
However, since $d_2$ and $f_2$ assign False to B(2) and $d_3$ and $e_3$ assign True to B(2), none of the 2nd level solutions that extend a 1st level solution have extensions of the 3rd level. Therefore, the procedure terminates because we have reached a point where none of the finite number of level 1 solutions have extensions beyond the second level. This reveals the formula to be, in Skolem’s words, ``contradictory’’, despite the fact that it is satisfiable in the domain $\{0,1,2\}$.
The other possibility is for the procedure to reach a level $n$ such that the level 1 solutions that have extensions of level $m+1$ are the same as those that have extensions of level $m$. Since (for formulas with this prefix) the assignment of truth values to the atomic components of level $n$ is independent of the assignment of truth values to atomic components of all levels earlier than $n-1$, the formula is revealed to be ``consistent’’.
Question: Am I misrepresenting this procedure or does Skolem really intend to rule out formulas that are consistent (i.e. satisfiable) but do not have infinite models? If so, how can this be used as a decision procedure for satisfiability?
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.
Skolem is working in the context of first-order logic without equality, so any theory with a finite nonempty model has an infinite model. Namely, you can just add infinitely many indistinguishable copies of one of the elements of your model.
In any case, though, you seem to be misunderstanding the logic here. Carrying out the first $n$ steps of the procedure successfully does not prove that there exists a model with domain $\{0,\dots,n\}$. Instead, it proves there is an "almost-model", where your sentence $\forall x\exists y[\ldots]$ is satisfied as long as you aren't allowed to pick $x=n$. Namely, if you pick $x$ to be any $i<n$, then you can take $y=i+1$. But for $x=n$, there might not be any $y$ that works. That's what the next step of the construction is for: it is checking whether you can have an element $y$ that works for $x=n$ as well. (The construction labels this element $y$ as $n+1$ as if it were a new element, but it might turn out to just be an indistinguishable copy of an element that you already had, so that you could reduce your final model down to a finite one by reversing the process described in the first paragraph.)