Berka I 58
Normalform/Berka: Folgendes Verfahren soll Wahrheitstabellen ersetzen: die ausgezeichnete (kanonische) Normalform: Hilbert/Ackermann (1928).
Berka I 112
Def überführbar/Hilbert/Berka: in eine andere überführbar heißt, eine Formel wenn die Äquivalenz der beiden ableitbar ist.
Def pränex/Hilbert: Eine Formel ist pränex, bei der alle Quantoren am Anfang stehen und die Bereiche (Reichweiten) sich bis zum Ende erstrecken.
Def deduktionsgleich/Hilbert: Zwei Formeln heißen deduktionsgleich, wenn jede aus der anderen ableitbar ist.
Jede Formel ist einer jeden solche Formel deduktionsgleich, die aus ihr entsteht, indem jede freie Individuenvariable (IV) durch eine vorher nicht auftretende gebundene Variable ersetzt wird und die zu den eingeführten gebundenen Variablen gehörigen Allzeichen (Allquantoren) (in beliebiger Reihenfolge) an den Anfang gestellt werden. ("Austausch der freien Variablen gegen gebundene").
Das geht auch in umgekehrter Reihenfolge.
Def Skolemsche Normalform/SN/Hilbert: Die Skolemsche Normalform ist eine eine pränexe Formel (d.h. alle Quantoren sind am Anfang, Reichweiten bis zum Ende), bei der unter den voranstehenden Quantoren nirgends ein Allquator vor einem Existenzquantor steht.
Jede Formel ist einer Skolemschen Normalform deduktionsgleich.
(s) D.h. Jede Formel kann zu einer Skolemschen Normalform umgeformt werden.
Berka I 116
Anmerkung: Diese Skolemsche Normalform ist die "beweistheoretische".
Def erfüllungstheoretische Skolemsche Normalform/Hilbert: Die erfüllungstheoretische Skolemsche Normalform ist dual zur beweistheoretischen Skolemschen Normalform, d.h. die Allquantoren und Existenzquantoren tauschen ihre Rollen. (>
Dualität).
Einsetzen/Hilbert/(s): Das Einsetzen wird hier auf freie Variablen angewendet.
Umbenennung/Hilbert/(s): Die Umbenunng wird hier auf gebundene Variablen angewendet
(1).
1. D. Hilbert & P. Bernays: Grundlagen der Mathematik, I, II Berlin 1934-1939 (2. Aufl. 1968-1970).
