Books on Amazon
|Berka I 113
Derivation/Inserting/"Evidence threads"/Hilbert: every derivation can be dissolved into evidence threads, that is, we start with the final formula by applying the schemes (α), (β). (...).
N.B.: then by the dissolution of a derivative into evidence threads, one can put back the insertions into the initial formulas.
Inserting/Insertion rules/Variables/evidence threads/Hilbert: We can do without rules of insertion by putting back the insertions (by means of evidence threads). For from the derivation of formulas which do not contain a formula variable, we can eliminate the formula variables altogether, so that the formally deductive treatment of axiomatic theories can take place without any formula variables.
Hilbert: the rule that identical formulas of the propositional calculus are allowed as initial formulas is modified in such a way that each formula which results from an identical formula of the propositional calculus is permitted as an initial formula.
Evidence threads(s): the rule of insertion also becomes superfluous by the fact that one can study the practical application in the course of time. That is, each case is documented, so you do not need a rule for non-current cases.
In the place of the basic formula
(x)A(x) > (A(a) is now: (x)A(x) > A(t)
and in the place of
(Ex)A(x) is now: A(t) > (Ex)A(x)
Formulas: That is, formulas are replaced by formula schemes.
Axioms are replaced by axiom schemata.
In the axiom schemata, the previous free individual variables are given by designations of arbitrary terms, and in the formula schemes, the preceding formula variables are replaced by arbitrary formulas.
K. Berka/L. Kreiser
Logik Texte Berlin 1983