76 Der engere Funktionenkalkül.

Die in Rede stehende Behauptung besagt nun, daß aus
MS GZWW LD

nicht B (=, Ger)
bewiesen werden kann. In dieser Behauptung kommt die sachlich-
geometrische Bedeutung von =, Ger, Zw, Eb nicht mehr vor. Denn
entsprechend dem axiomatischen Standpunkt darf ja beim Beweise
eines Satzes aus den geometrischen Axiomen nichts anderes von den
eingeführten Grundbeziehungen benutzt werden, als was in den Axiomen
ausdrücklich formuliert ist.

Wir können daher diese Prädikate ganz eliminieren und an ihre
Stelle vier variable Prädikate — natürlich mit der entsprechenden
Zahl von Argumenten — setzen:

DA ) SE Z W RN

Die Beweisbarkeit des Pascalschen Satzes würde bedeuten, daß
für irgend vier solche Prädikate F,G, H, K, für welche

EG MK
wahr ist, auch stets (F, G) wahr ist, daß also
ME G H K EG

eine allgemeingültige logische Formel ist. Es handelt sich also darum,
zu erkennen, daß dies nicht der Fall ist. Im Falle der Bekanntheit
eines allgemeinen Entscheidungsverfahrens für die Gültigkeit logischer
Formeln wäre nun diese Aufgabe auf einem vorgeschriebenen Wege
zu lösen, so daß man sich das Suchen nach einem besonderen Unab-
hängigkeitsbeweise für den Pascalschen Satz ersparen könnte.

Auf dieselbe Weise ließe sich für jeden anderen geometrischen
Satz feststellen, ob er eine logische Folge der Axiome ist oder nicht.
Auch Fragen der Widerspruchsfreiheit würden sich an Hand des Ent-
scheidungsverfahrens lösen lassen. Z.B. ist die Frage, ob die in der
Formel

W, Ger Zw, . Eb)
zusammengefaßten geometrischen Axiome miteinander logisch ver-
träglich sind, gleichbedeutend mit der anderen, ob die Bedingung

(F, G, H, K)

durch Prädikate
FÜ WE G B R K y
überhaupt erfüllbar ist oder, anders ausgedrückt, ob die Formel

XF, G, H, K)