On the decision problem for the functional calculus of logic (1933i)
Solomon Feferman, John W Dawson, Stephen Cole Kleene, Gregory Martin Moore, Robert M Solovay, Jean van HEIJENOORT · 2001
Abstract The introductory note to 1999i, as well as to related items, can be found on page 226, immediately preceding 1992a.In Ergebnisse eines mathematischen K olloquiums ( 1992a) I briefly sketched a procedure by which one can decide, for each formula of the restricted functional calculus1 that in normal form contains only two ( and in fact adjacent) universal quantifiers, whether it is satisfiable.2 L. Kalmar then dealt with that case of the decision problem in detail by using the same method.3 In the case of one universal quantifier, a case which had been treated earlier by P. Bernays, M. Schonfinkel and W. Ackermann, it turned out that such formulas, if they are satisfiable at all, are satisfiable already in a finite domain of individuals. The goal of the investigation that follows is to prove this also for the case of two universal quantifiers. Secondly, it will be shown that solving the next more complicated case ( three universal quantifiers) would already be equivalent to solving the full decision problem (see below, page 322).