Skolem's method for checking truth-value assignments - a "cut-free proof procedure" for first-order logic?

Question

In his intro to ( Skolem 1923a), Van Heijenoort (From Frege to Godel, p. 509) describes Skolem as giving “an alternative to the axiomatic approach” to proving a first-order formula. This is referring to the effective procedure Skolem gives for checking whether or not a first-order formula U has a solution of level n. A solution of level n is an assignment of truth-values to the atomic propositions of the nth level expansion. The nth level expansion of U is the conjunction of instances of U formed by dropping the quantifiers, letting the universal variables range over the domain of level n-1, and introducing new integers for the existential variables.

Skolem's procedure is as follow:

1. Form the expansions of U up the nth level.
2. At each level, write down all possible truth-value assignments to the atomic propositions.
3. If a truth-value assignment at level m has no continuations at level m+1, reject it.

U has a solution of level n if and only if there are truth-value assignments remaining when this procedure is carried out up to level n. If for some n there is no solution of level n, then we have shown that U is truth-functionally unsatisfiable.

VH says that this procedure “provides proofs that are cut free and have the subformula property”. I know what those properties are in the context of the sequent calculus, but I don’t understand what he means in this context.

References:

SKOLEM, THORALF

[1923a] Einige Bemerkungen zur axiomatischen Begründung der Mengenlehre. Matematikerkongressen i Helsingfords den 4–7 Juli 1922, Den femte skandinaviska matematikerkongressen, Redogörelse . Helsinki: Akademiska Bokhandeln, 1923, pp. 217–232. English translation in van Heijenoort (ed.) [1967], pp. 290–231.

VAN HEIJENOORT, JEAN

[1967a] From Frege to Gödel; a source book in mathematical logic, 1879-1931. Cambridge, Harvard University Press.

Answer 1

The answer to the question can be found in Section I (especially p.11) of this source (it is a newly typeset version of Joseph E. Quinsey's 1980 Oxford doctoral thesis Some Problems in Logic: APPLICATIONS OF KRIPKE’S NOTION OF FULFILMENT).