Berka I 113
Derivation/insertion/"evidence threads"/Hilbert: any derivation can be dissolved into evidence threads, that is, we start with the final formula by applying the schemes (α), (β), (...).
I 114
N.B.: then by the dissolution of a derivative into evidence threads, one can put back the insertions into the initial formulas.
>
Proofs, >
Provability, >
Derivability.
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 contain no 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.
>
Inserting.
Hilbert: the rule that identical formulas of the propositional calculus are permitted as initial formulas is modified in such a way that each formula which results from an identical formula of the propositional calculus by insertion is permitted as the initial formula.
Evidence(s): the rule of insertion is also 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:
Instead of the basic formula
(x)A(x) > A(a) is now: (x)A(x) > A(t)
And in place of
(Ex) A (x)
is now: A(t) > (Ex)A(x)
t: term.
Formulas are replaced by formula schemes.
Axioms are replaced with axiom schemata.
In the axiom schemata, the previously free individual variables are replaced by designations of arbitrary terms, and in the formula schemes, the preceding formula variables are replaced by arbitrary formulas
(1).
>
Schemes, >
Axioms, >
Axiom systems.
1. D. Hilbert & P. Bernays: Grundlagen der Mathematik, I, II, Berlin 1934-1939 (2. Aufl. 1968-1970).
