In the first paper of the above main title, one of us has proved that any formula of the first order predicate calculus is equivalent (as to being satisfiable or not) to some binary first order formula having a prefix of the form (Ex1)(x2)(Ex3) … (xn) and containing a single predicate variable. This result is an improvement of a theorem of Ackermann stating that any first order formula is equivalent to another with a prefix of the above form but saying nothing about the number of predicate variables appearing therein. Hence the question arises if other theorems reducing the decision problem to the satisfiability question of the first order formulas with a prefix of a special form can be improved in like manner. In the present paper we shall answer this question concerning Gödel's reduction theorem stating that any first order formula is equivalent to another the prefix of which has the form

The philosophical dispute over whether there are universale, or abstract entities, is not a dispute over the admissibility of general terms. Both sides will agree that general terms, e.g. ‘man,’ and perhaps even abstract singular terms such as ‘mankind’ and ‘7’, are meaningful, in the sense at least of participating in statements which as wholes are true or false. Where the platonists (as I shall call those who accept universale) differ from their opponents, the nominalists, is in positing a realm of entities, universals, corresponding to such general or abstract words.

The platonist is likely to regard the word ‘man’ as naming a universal, the class of men or the property of being a man, much as the word ‘Caesar’ names the concrete object Caesar. Actually, however, this is an extraneous detail. The platonist could equally well concur with the nominalist in the view that general terms, though meaningful in context, are not names at all.