68 Der engere Funktionenkalkül.

Endlich kommen wir zu )7). Ein Ausdruck
U —> B(x)
geht (falls %X keine freie Variable enthält) durch unsere Umformung
über in
(x)(4—> B (x)),
(A—>B(1) & (A — B(2))
usw. —> (x)B(x) verwandelt sich in:
MDA KB2)

Beide Formeln sind aber nach den Regeln des Aussagenkalküls
äquivalent. Ebenso ist es, falls W noch freie Variablen enthält. Ent-
sprechendes gilt für die Regel y), soweit sie das Hinzufügen eines
Existentialzeichens betrifft.

Wir haben damit tatsächlich gezeigt, daß jede aus den Axiomen
ableitbare Formel durch unsere Umformung in eine immer richtige
Aussagenverbindung übergeht.

(Ex)F(x) > (x) F(x)
hat nun diese Eigenschaft nicht, denn die Umformung dafür lautet:
FU A(2) 3A Q
Av Br A&B
und dies ist keine immer richtige Aussagenformel.

Wir haben damit die Unvollständigkeit unseres Axiomensystems
gezeigt.

Ob das Axiomensystem wenigstens in dem Sinne vollständig ist,
daß wirklich alle logischen Formeln, die für jeden Individuenbereich
richtig sind, daraus abgeleitet werden können, ist eine noch ungelöste
Frage. Es 1äßt sich nur rein empirisch sagen, daß bei allen Anwendungen
dieses Axiomensystem immer ausgereicht hat. Die Unabhängigkeit
der einzelnen Axiome ist noch nicht untersucht worden,

$ 10. Beispiele für die Anwendung des Funktionenkalküls
zu formalen Beweisführungen.

Wir haben den Funktionenkalkül bisher nur benutzt, um logische
Formeln, in dem in 86 erklärten Sinne, abzuleiten. Die Prämissen
unserer Schlüsse, die Grundformeln a) bis f) waren dabei selbst wieder
rein logischer Natur. Wir wollen nun die allgemeine Methode der for-
malen Ausführung logischer Schlüsse im Funktionenkalkül, die wir vor
der Aufstellung der Axiome nur andeutungsweise beschreiben konnten,
an ein paar Beispielen darlegen. Das allgemeine hierbei anzuwendende
Verfahren besteht darin, daß die Prämissen der Schlüsse symbolisch