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 (α), (β), (...).
>
Derivation, >
Derivability.
I 114
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). 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.
>
Proofs, >
Provability.
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.
Hilbert:
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)
t: term.
Formulas are replaced by formula schemes.
Axioms are replaced by axiom schemata.
In the axiom schemata, the previously free individual variables are given by designations of arbitrary terms, and in the formula schemes, the preceding formula variables are replaced by arbitrary formulas
(1).
>
Axioms, >
Axiom systems.
1. D. Hilbert & P. Bernays: Grundlagen der Mathematik, I, II, Berlin 1934-1939 (2. Aufl. 1968-1970).