ON CHARACTERIZATIONS AND UNDECIDABILITY OF THE FIRST-ORDER FUNCTIONAL CALCULUS
Juliusz Reichbach · Institutional Repositories DataBase (IRDB) · 1965
In publications $[81, [9]$ I have presented some semantic characterizations of theses of the first-order functional calculus. In connection with ones the present paper describes more strong characterizations of the theses: 1. By means of new proof rules which kind is different from the usual ones, we obtain an important syntactic characterization; in this way we reduce the decidability problem to consistency of families of sets of atomic formulas such that indices of variables occurring in those formulas are $\leq 3^{1}$ . 2. In connection with the syntactic characterization we obtain new semantic characterization which shows that in the decidability problem we may restrict our considerations only to families of models which domains have $\leq 3$ elements,