My question concerns a statement by Gödel in 1967. Commenting on Skolem’s failure to infer completeness from his (1922) proof of the Lowenheim-Skolem theorem, Gödel observes that Skolem
did not give a correct proof of that completeness theorem which he explicitly stated (op. cit., p. 134), namely that there is a contradiction at some level n if there is an informal disproof of the formula. (Letter to Wang, in Wang 1974*, p. 10)
Background: As I understand it, Gödel’s own (1930) completeness proof proves the version: a formula $A$ is either refutable or satisfiable. The proof relies on the method, taken from Löwenheim and Skolem, of "expanding" $A$ into an indexed series of quantifier-free conjunctions of its instances, with existential variables replaced by functional terms (this is a gloss). These expansions are subject to the completeness of propositional logic: either some $A_n$ is refutable by the truth-table method, or $A_n$ is satisfiable for every n. In the second case, a model can be constructed from the satisfying assignments guaranteed for each $A_n$. In the first case, Gödel shows that the satisfiability of $A$ implies, for every $n$, the satisfiability of the expansion $A_n$. So, if $A_n$ is refutable for some $n$, then $A$ is refutable.
My question is as follows: in the quote above Gödel states the theorem as: if $\sim A$ is provable, then there is an $n$ such that $A_n$ is contradictory, "provable" taken in an informal sense. We can infer from $A_n$ being contradictory that $A$ is not satisfiable (the quote continues: "evidently a correct informal disproof implies the nonexistence of a model"). If $A$ is not satisfiable then $\sim A$ is valid. But this is a statement of soundness then, not completeness. Am I confused about something?
*Wang, Hao. From mathematics to philosophy. London: Routledge & Kegan Paul.
