8 11. _ Das Entscheidungsproblem im Funktionenkalkül. 75

Gerade, die in der Ebene eines Dreiecks liegt, eine Seite dieses Dreiecks
schneidet, so schneidet sie auch eine andere Seite dieses Dreiecks‘‘,
entspricht die folgende Formel:
(x) (y) (z) (u) (v{[Eb(x, y, z, u) & Ger (x, y, 2) & Zw (v, x, y)
& Ger (x, y, u) & Ger (z, u, v)]
—> (Ew)[Ger (u, v, w) & (Zw (w, x, z) v Zw(w, y, 2)) }}.
Zu beachten ist bei der Einführung der Beziehungen „Ger‘ und „Eb“,

daß für diese die Symmetrieeigenschaften als Axiome formuliert werden
müssen. So hat man die Formel

(x) (y) (z){Ger (x, y, z) > (Ger (x, z, y) & Ger (y, %, 2))}

und die entsprechende für Eb aufzustellen. Die Eigenschaften der
Indentitätsbeziehung sind ebenfalls als Axiome zu formulieren :
(x) = (%, %),

(x) (y) (2) {= (&, 2) & = (y, z) > = (%, },
(%, 4) &GEL(X,.Y, z)) — Ger (u, y, 2)},
(x, v) & Eb(x, y, z, u)) —& Eb(v, y, Z, u)}.
x, y) & Zw(x, u, z)) — Zw(y, u, 2)}-
%, y) & Zw(u, x, z)) — Zw (u, y, 2)}-

) :
(x) (y) (2) (4) ({
) («) (2){(=
(x) (y) (w) (2){C

Die vier letzten Formeln bringen zum Ausdruck, daß in jeder vor-
kommenden Beziehung Identisches füreinander gesetzt werden kann.

Denken wir nunı uns alle in Formeln geschriebenen Axiome durch
&-Zeichen zu einer einzigen Formel verbunden. Diese stellt die Gesamt-
bedingung dar, welcher die Prädikate s = . G . Zw ... .E6'; unters
worfen sind oder, wie man sich in der Axiomatik auch ausdrückt, sie
enthält die implizite Definition dieser Prädikate. Zur Abkürzung für

diese Formel möge

I

(
(

A =, Ger, Zw, Eb)

geschrieben werden.

Der spezielle Pascalsche Satz lautet in der gewöhnlichen Ausdrucks-
weise folgendermaßen : Es seien ABC und A’B’C’ je drei Punkte auf zwei
sich schneidenden Geraden. Alle genannten Punkte seien vom Schnitt-
punkt der beiden Gerade verschieden. Ist dann BC’ parallelzuCE/ und
CA’ parallel zu AC’, so ist auch AB’ parallel zu BA’. — Dieser Satz
Jäßt sich wieder durch eine logische Formel darstellen, wobei von den
Prädikaten nur = und „Ger‘“ auftreten. Wir wollen diese Formel mit
%® (=, Ger) bezeichnen. :