[FOM] Historical query (on the very idea of a formalized theory)

[Richard Zach]

> > I was wondering: at what point between did people become explicit and clear 
> > about this sort of effectiveness requirement on a properly formalized 
> > theory?
> 
> I believe it is first made explicit in von Neumann, ``Zur Hilbertschen
> Beweistheorie'' Mathematische Zeitschrift 26 (1927): 1--46.

[snip]

I downloaded the paper, so here's some more detail:

In Section I A.3, "Formulas" von Neumann does the following:

- Give a precise inductive definition of what formulas are
- State that it is decidable if a given sequence of symbols is a formula
or not
- State that there is a unique way each formula can be obtained from the
inductive formation rules (unique readability)

In Section I A.4, "Basic properties of formulas" he:
- gives precise definitions of subformulas, free and bound occurrences
of variables, and substitution

Section I B.1, "Proving and Consistency" contains the things you're
interested in (my, rough, translation):

[quote]
"Suppose a procedure R is given, on the basis of which certain normal
forms [= sentences] can be formed. We call this procedure R the axiom
rule, and the formulas formed on the basis of R, axioms.

The axiom rules which we in fact apply (i.e., the axiom rules of our
formalistic mathematics), will be constituted so as to allow to decide
of any given normal form whether it is an axiom or not, i.e., whether it
is possible to form it with the help of R.  This fact is, however,
immaterial here.

If now an axiom rule R is given, then we define the provability of
normal forms as follows (inductively):

I. If the normal form a is an axiom, it is provable.
II. If the two normal forms a and a -> b are already recognized to be
provable, then also the normal form b is provable.

Note: As in the definition of formula in \S I A 3, also here we have an
inductive definition.  This only allows only the positing of provable
normal forms, but not necessarily the decision whether a given normal
form is provable.  It may perhaps be possible to find a procedure on the
basis of the definition which does perform this; this, however, depends
on the specific properties of the definition.  We saw, e.g., that it is
possible for the definition of a formula.  For the definition it is so
far undetermined, since the axiom rule is not yet given. It could be
that this decidability already does not hold for the axiom rule.  But
even when it holds (as it will be the case for the axiom rule to be used
in the following), nothing at all is settled.  For part II of the
definition is here of a significantly different character as it was in
the definition of formula. [...] While there everything old is included
in the new, this is very much not the case here: b itself does not stand
in any relation to a, which was used in its production (its "proof"),
and only in a partial relation to a -> b.  Looking at b, one cannot see
from which a, a -> b it was formed ("proved").
[endquote]

Of course, the requirement that it should be decidable if a given
formula is an axiom, and if a given sequence of formulas is a proof is
implicit in Hilbert's writings before then.  But I suspect von Neumann
was the first to state it explicitly, since he considered axiomatic
systems (with respect to provability questions, as opposed to
"realizations" ie models) in general, whereas Hilbert and others had
always considered specific axiom systems.  It could be that there is
something in Julius König's 1914 book (Neue Grundlagen der Logik,
Arithmetik und Mengenlehre), but that I don't think is online, so it'll
take me a while to check.