Books on Amazon
|Berka I 58
Normal form/Berka: the normal form is another method to replace truth tables: excellent (canonical) normal form: Hilbert/Ackermann (1928).
Berka I 112
Definition convertible/Hilbert/Berka: convertible into another means is a formula when the equivalence of the two is derivable.
Definition pranex/Hilbert: pranex is a formula in which all quantifiers are at the beginning and the ranges extend to the end.
Definiton deduction-equal/Hilbert: deduction-equal are two formulas, if each is derivable from the other.
Each formula is deduction-equal to each such formula, which results from it by replacing any free individual variable (IV) with a bound variable which has not previously occurred, and the universal quantifier belonging to the introduced bound variables (in any order) are placed at the beginning. ("Exchange of free variables against bound ones").
This can also be done in reverse order.
Definition Skolem's normal form/SN/Hilbert: a prenexic formula (that is, all quantifiers at the beginning, range to the end), where there is nowhere among the previous quantifiers a universal quantifier before an existential quantifier.
Each formula is deduction-equal to a Skolem normal form.
(s). Each formula can be transformed into a Skolem normal form.
Note (I 116) This Skolem normal form is the "proof-theoretic" one.
Definiton fulfillment theoric Skolem normal form/Hilbert: is dual to the proof-theoretic Skolem normal form: i.e. The universal quantifiers and existence quantifiers exchange their roles. (> Duality)
Berka I 116
Insert/Hilbert/(s): inserting is used here for free variables.
Rename/Hilbert/(s): renaming is used here for bound variables.
K. Berka/L. Kreiser
Logik Texte Berlin 1983