[FOM] Formation Rules

[Max Weiss]

Edwin Mares asked

>>> Who was the first logician to present rigorous formation rules  
>>> for a formal language? And where (and when) did they do it?

And Heck replied

>> if one were to rephrase the question as "Who was the first  
>> logician to give rigorous formation rules for a language of  
>> reasonable expressive power?" then the answer is definitely: Frege.

In particular Heck says that the place where Frege gave these rules  
is in the Grundgesetze, sections 28 and 30.  I think he's right about  
Frege's intention thereabouts.

Let me ask a further question: are the formation rules Frege gave  
there correct?  (Of course, this wasn't Mares' question, but it seems  
relevant.)

The Fregean notions of name and of proper name (henceforth "Bg  
(proper) names") are analogous to the notions of formula and  
sentence, if we reinterpret placeholders as free variables.  (I  
didn't appreciate this before.)  So a sufficient condition for a  
resounding answer of "Frege" to Mares' question is that Frege  
inductively characterized the Bg names.

(Of course there may be another sufficient condition, such as e.g.  
that Frege nearly successfully characterized the Bg names, or that he  
successfully defined "Bg proper name".)

In Gg S30, which Heck pointed out, Frege describes "two ways to form  
a name" and concludes "all correctly-formed names are formed in this  
manner."  Given the list of primitives at the beginning of S31, this  
looks like an inductive specification (indeed with a closure clause).

But I have trouble seeing how Frege's formation rules suffice to  
generate all Bg-names.

I hope that, for present purposes, it will not misrepresent the  
situation to stipulate that a "Bg function name" is a Bg name that  
results from replacing, in a Bg proper name, some occurrences of Bg  
names with placeholders of the same type.  (*We* can define "Bg  
proper name" independently.)

Construed under the stipulation, Frege's rules permit exchanges of Bg  
names for placeholders of the same type, and vice versa.  Frege puts  
restrictions on the types for which the exchanges can be made.  I'm  
worried that these restrictions are too strong.

Here are the restrictions. In one direction, occurrences of a  
placeholder X in a name Y can be replaced with a constant Z only if X  
and Z are of the same type and either:
	Z is a proper name and Y is first-level one-place function name, or
	Z is a first-level function name and Y is a second-level one-place  
function name, or
	Z is a second-level function name and Y is a third-level one-place  
function name, or
	Z is a proper name and Y is a first-level two-place function name.
In the other direction, some occurrences of a name X in a name Y can  
be replaced with a placeholder Z only if X and Z are of the same type  
and X is a proper name.

Given these restrictions, I can't see how to form the proper name
	"forall f forall x (fx = fx)".

This may be due to my thickness.  But if someone could show how  
Frege's account is supposed to work, we would have a more definitive  
answer to Mares' question.

Thanks,

Max