[FOM] Formation Rules

Richard Heck rgheck at brown.edu
Tue Oct 17 15:06:15 EDT 2006

Edwin Mares wrote:
>> Who was the first logician to present rigorous formation rules for a formal language?
>>And where (and when) did they do it?
Richard Zach wrote:
> It depends on your standards for "rigorous".  Neil Tennant's standards are apparently 
>higher than Richard Heck's, so you may or may not be willing to count
Frege.  But if what
>you mean is something that explicitly involves "If A and B are formulas, then A & B is a 
>formula" a probable answer is: Hilbert in the lecture course "Prinzipien der Mathematik" 
>(Göttingen, Winter Semester 1917/18) (pp. 130-131 of the lecture notes).

True. I took "rigorous" to mean: rigorous by ordinary mathematical
standards; sufficient for the purposes of actual proof; not just hand
waving that serves no real purpose. I think a reasonably charitable
reading will show that Frege does that much, though there is of course
much that he does not do. He does not say, "If A and B are formulae...",
because the syntax of his system is different. What he says is, e.g.,
that a "name" can be formed from a one-place functional expression and a
"name"; or from a two-place functional expression and two "names"; and
Frege gives a very careful explanation of what functional expressions
are (as I mentioned, the discussion of complex predicates is
particularly subtle), and he is equally careful about conflicts of
variables and the like. It's not up to the standard Neil had in mind, to
be sure, but I'd be surprised if it was all that far from Hilbert, once
one adjusts for the differences in the underlying conceptions of syntax.

On a related note, Neil mentioned the "closure" condition. Frege doesn't
mention that explicitly, and that's certainly a lack of rigor. On the
other hand, he does use proof by induction on the complexity of
expressions, and, given his concern with formalizing induction, it is
hard to imagine he didn't realize what he was doing: defining the class
of "correctly formed names" by an inductive definition that could, in
turn, be formalized using the ancestral if one were so inclined.


Richard G Heck, Jr
Professor of Philosophy
Brown University
Get my public key from http://sks.keyserver.penguin.de
Hash: 0x1DE91F1E66FFBDEC
Learn how to sign your email using Thunderbird and GnuPG at:

More information about the FOM mailing list