v Der engere Funktionenkalkül.

Durch Umbenennung der Variablen erhält man aus den beiden
Voraussetzungen :

1. (Ew) Dl(u, v, w) .
2. (P(x, u, y) & D(u, v, w) & D(y, v, z)) — Dlx, w, 2).

Wendet man auf die zweite Voraussetzung die Regel VIl; S.28 an,
so kann man sie umformen zu:

Dl(u, v, w) — [((I)(x‚ u, y) & D(y, v, z)) — D(x, w, z)].

Unter Benutzung der zu Formel (34) gehörigen Regel kann man daraus
ableiten:

(Ew) D(u, v, w) — (Ew) [(D(x, u, y) & D(y, v, z)) — D(x, w, z)].

Da nun (Ew)P(u, v, w) als richtig angenommen wurde, so ergibt sich
weiter
(Ew)(D(x, u, y) & D(y, v, z) — Dl(x, w, z)).

Daraus ergibt sich die Behauptung, indem man nach Regel y’ die All-
zeichen (%) und (v) vorsetzt.

$ 11. Das Entscheidungsproblem im Funktionenkalkül und
seine Bedeutung.

Nach der durch die letzten Beispiele gekennzeichneten‘ Methode
kann man den Funktionenkalkül insbesondere zur axiomatischen Be-
handlung von Theorien verwenden. Für diesen Zweck ist der Kalkül
sehr geeignet. Infolge der streng formalen Behandlungsweise wird
nämlich verhütet, daß bei der Ableitung aus den Axiomen versteckte
Voraussetzungen mitbenutzt werden.

Die mathematische Logik leistet aber noch mehr als eine Ver-
schärfung der Sprache durch die symbolische Darstellung der Schluß-
weisen. Nachdem einmal der logische Formalismus feststeht, kann man
erwarten, daß eine systematische, sozusagen rechnerische Behandlung
der logischen Formeln möglich ist, die etwa der Theorie der Gleichungen
in der Algebra entsprechen würde.

Eine ausgebildete ‚„,Algebra der Logik‘“ begegnete uns im Aus-
sagenkalkül (man vgl. insbesondere $ 4—09 des I. Kapitels). Die
wichtigsten der dort erwähnten und gelösten Probleme waren das der
Allgemeingültigkeit und der Erfüllbarkeit eines logischen Ausdrucks.
Beide Probleme zusammen pflegt man auch kurz als das Entscheidungs-
problem zu bezeichnen.

Bei dem Problem der Allgemeingültigkeit handelt es sich um die
folgende Frage: Wie kann man bei einem beliebigen vorgelegten logischen
Ausdruck, der keine individuellen Zeichen enthält, feststellen, ob _ der Aus-