[FOM] Historical query (on the very idea of a formalized theory)
Richard Zach
rzach at ucalgary.ca
Wed Dec 1 14:11:34 EST 2004
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
More information about the FOM
mailing list