Ein Verfahren der mathematischen Logik. (Q2595478)

Verf. gibt ein Verfahren an, das zu jedem Zählausdruck in der pränexen Normalform einen bezüglich der Erfüllbarkeit gleichwertigen Zählausdruck der Form \[ (x)\;(y)\;(Ez)\,F(z, x, y)\,\&\;(x_1)\cdots(x_r)\,\mathfrak A(x_1, \dots ,x_r) \] zu konstruieren gestattet. Dabei ist \(F\) die einzige Prädikatvariable, die zu den im ursprünglichen Ausdruck vorkommenden Prädikatvariablen hinzukommt. Statt der dreistelligen Prädikatvariablen \(F\) kann man auch zwei zweistellige Prädikatvariable nehmen. Man erhält dann als Normalform \[ (x)\;(y)\;(Ez)\,\bigl(R_1(z, x)\,\&\,R_2(z, y)\bigr)\,\&\,(x_1)\cdots(x_r)\,\mathfrak A(x_1,\dots,x_r). \]