Untersuchungen über das Eliminationsproblem der mathematischen Logik. (Q2616499)

Nach der erklärung des Verf. beschäftigt sich das Eliminationsproblem im allgemeinsten Sinne mit der Frage, wie man einen logischen Ausdruck durch einen äquivalenten ersetzen kann, dessen logische Struktur einfacher ist. Schon früher ist dies Problem gelöst worden, wenn bloß einstellige Prädikate vorkommen, nämlich in dem Sinne, daß man z. B. zu einem Ausdruck \((EF)U(F, A, B, C, \dots )\), wo \(U\) ein Zählausdruck ist, worin die Prädikatenvariablen \(F, A, B, C, \dots \) vorkommen, einen äquivalenten Zählausdruck \(V(A,B,C, \dots )\) finden kann. In \S 2 gibt Verf. eine Beispiele für die Elimination beim Vorkommen mehrstelliger Prädikate; er erhält auch in diesen Fällen einen Zählausdruck als Resultante. In \S 3 zeigt er aber, daß es nicht immer so ist; z. B. ist kein Zählausdruck mit \((EF)(Fx \& \bar {F}y \& (u)(v) \bar {F}uFv \bar {N}uv)\) gleichwertig. Dagegen ist dieser Ausdruck mit der gleichzeitigen Gültigkeit einer unendlichen Folge \(Z_1, Z_2, \dots \) von Zählausdrücken gleichwertig. Auf Grund dieser Erkenntnis erweitert Verf. in \S 4 den Begriff der Resultante. Eine Klasse von Zählausdrücken, deren gleichzeitige Gültigkeit mit dem gegebenen Ausdruck äquivalent ist, soll auch Resultante heißen, wenn man für jeden vorgelegten Zählausdruck entscheiden kann, ob er zur Klasse gehört oder nicht. Verf. zeigt in \S 4, daß einstellige Prädikate stets in diesem Sinne eliminierbar sind, falls nur Allzeichen für die Individuen auftreten, auch wenn sonst mehrstellige Prädikate vorkommen. Die Zählausdrücke der Resultatenklasse werden nach bestimmten Regeln aus den freien Prädikatenvariablen des gegebenen Ausdrucks aufgebaut. Im Falle eines wohlgeordneten Individuenbereichs kann er dann, wenn alle Zählausdrücke in jener Klasse erfüllt sind, zeigen, daß der gegebene Ausdruck wahr wird. In \S 5 wird die Elimination mehrstelliger Prädikate auf die Elimination einstelliger Prädikate zurückgeführt. In \S 6 wird gezeigt, wie man Seinszeichen für Individuen durch Allzeichen ersetzen kann, wenn man Funktionen einführt, deren Argument und Werte Individuen sind. In besonderen Fällen gelingt es dadurch, das Eliminationsproblem zu lösen, auch wenn Seinszeichen für Individuen vorkommen.