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 (negB(1) land A(0,0))$

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’’.footnote{In other words, if a formula of level $<m$ is consistent with a solution of level $m$, no solution of level $m+1$ or higher will render it inconsistent, since new inconsistencies will only occur between levels $m$ and higher.}

**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.