60 Der engere Funktionenkalkül.

mel (6) in (x) F(x) — (x) G(x) verwandelt werden. Da (x) F(x)  (Ex) F(x),
(x) G(x) > (Ex)G(x), so folgt dann die gesuchte Formel.

Der Formel (34) entspricht die folgende Regel: Ist YA(x) — B (x)
beweisbar, so kann man auch (Ex)Y(x) — (Ex)®(x) ableiten. —

Man erhält nämlich aus Y(x) — B(x) nach Regel /

(x)(A(x) —> B (4)),
und unter Benutzung von (34): (Ex)2(x) — (Ex)(x).

Ganz ebenso wie aus (31) die Formel (32) abgeleitet wird, erhält
man aus (34) die Formel
O5 (2)(F(x) > G(x)) —> ((Ex) F(x) > (E x)G(x)).

Formel (35): (x)(F(x) — A) > ((Ex)F(x) > A4).

Beweis: (x) (F(x) —> 4) ist eine Abkürzung für (x)(F(x) v 4).

Es gilt nun die Formel

(x)(F(x) v 4) > (x)F(x) v 4,
die man ähnlich wie die Formel (26) beweist.
(x)E(x) &> (Ex) F(x),
(x)F(x) v A > (Ex) F(x) v 4.
Schreibt man nun wieder die Abkürzung —, so ergibt sich (35).

Formel (36): (Ex) (y)F(x, y) — (y) (Ex) F(x, y).

Das ist die schon früher erwähnte Vertauschungsformel, von der
auch bereits hervorgehoben wurde, daß sie nur als einseitige Folge-
beziehung gilt.

Beweis: F(x, y) — (Ex)F(x, y) (Einsetzung in Axiom f)],

(y)(F(x, y) — (Ex)F(x, y)) [Regel '7')].
Unter Benutzung von Formel (31) ergibt sich
(Y)-F(%, y) —> (y) (Ex) F(x, y),
(Ex) (y) F'(x, y) — (y) (Ex) F(x, y) [nach Regel 7)].

$ 7. Die Ersetzungsregel; Bildung des Gegenteils eines
Ausdrucks.

Nachdem wir eine Reihe von logischen Formeln abgeleitet haben,
sollen nun einige allgemeine Regeln besprochen werden, die zur Ge-
winnung eines Überblicks über das Gesamtsystem der logischen Formeln
besonders wichtig sind. Diese Regeln beziehen sich übrigens auf ganz
beliebige Ausdrücke unseres Kalküls. Sie gelten also auch für solche
Formeln, in denen individuelle Zeichen auftreten.