I'm a beginner in mathematical logic, and currently studying(myself, without any colleague, which is sad and so asking in here) basics of formal system. Before asking a question, I'll introduce my understandings of the concepts about collation and rules of formation.
My understandings.
Collation : A collation is a structure which comprised with placeholders. A placeholder is a representation of entry for strings. We denote a premise free placeholder by $\square$ and if we want to represent a placeholder which is quantified by a specific set of strings, we say a placeholder is a variable.
Rule of formation : A rule of formation, or simply a rule, is literally a rule which defines how to construct a collation. (and I don't know why do we have to know this concept. If someone gives you a collation, then the collation itself contains a rule, so I am thinking that a rule is not relevant concept.)
and a bonus,
Formal grammar : A Formal grammar, or simply a syntax, comprises of collations which determine WFF(Well Formed Formula) in formal language.
My Question.
As I mentioned above, I don't know why do we define a rule of formation, as it contained in the concept of collation. Of course, in the precondition that my understandings are correct (however, you can point me out if some of my understandings are wrong). What are the differences between a collation and a rule of formation?
You can see in ProofWiki Formal Language, with pointers to collation and formal grammar, where "collation" is exemplified with "words and the method of concatenation".
In the article about Formal language I've not found this term.
Personally, I think it is too complicated a way to present a formal system for mathematical logic.
You can see some textbooks, like :
and :
Roughly speaking, in mathematical logic we need the following concepts : alphabet, made of symbols, words (strings of symbols) and formulas : certain strings of symbols built up accordding to formation rules.