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

[Richard Zach]

On Tue, 2004-11-30 at 23:10 +0000, Peter Smith wrote:
> Church in his Intro. to Math. Logic (pp. 50 - 51) very clearly spells it 
> out that, for a properly defined "logistic system", the definition of a wff 
> has to be effective, the specification of the axioms has to be effective, 
> and it has to be effective what counts as a proof by the rules of 
> inference.
> 
> 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.  In footnote
78 of http://www.ucalgary.ca/~rzach/papers/history.html I wrote:

For instance, [in von Neumann 1927] the set of
well-formed formulas is given a clear inductive definition,
application of a function to an argument is treated as an operation,
and substitution is precisely defined.  The notion of axiom system is
defined in very general terms, by a rule which generates axioms
(additionally, von Neumann remarks that the rules used in practice are
such that it is decidable whether a given formula is an axiom).  Some
of these features von Neumann owes to König 1914.

I don't have the paper with me, so I can't double-check it right now.

-- 
Richard Zach ...... http://www.ucalgary.ca/~rzach/
Associate  Professor,   Department  of  Philosophy
University of Calgary, Calgary, AB T2N 1N4, Canada