Can a formal language always be generated by a formal grammar? 
*

*A formal language is often defined by means of a formal grammar. I
wonder for a formal language if there is always a formal grammar
that generates the language?

*Does this answer have something to do with "it is not possible to
design a recognizer(automaton) for certain formal languages"?


Thanks and regards!
Added: The definition I know for formal grammar is http://en.wikipedia.org/wiki/Formal_grammar#Formal_definition . Are there different definitions?
 A: In the most general definition, a formal language is simply an arbitrary set of strings over a particular alphabet. Assuming the alphabet is nonempty, that means there will be infinitely many strings and thus uncountably many sets of strings. There are only countably many formal grammars, so many sets of strings (formal languages) are not definable by formal grammars. 
Sometimes authors back away from the most general definition and require that the alphabet has to be countable or finite and the language has to be at least computably enumerable. In that case, you have to have a more specific definition of what a "formal grammar" is to make the question precise. Every c.e. language is generated by an "unrestricted grammar" in the sense of the Chomsky hierarchy, and every language generated by any grammar is c.e., so those classes of languages coincide. But, for example, not every c.e. language is a regular language in the sense of the Chomsky hierarchy. 
A: No. If you mean what I think you mean by "formal grammar," then there are only countably many formal grammars but uncountably many formal languages. Similarly, there are only countably many Turing machines, so most formal languages cannot be recognized by any Turing machine. 
(This is perhaps the simplest proof that there exist undecidable problems. Of course, the Halting theorem provides both a vivid and important explicit example of such a problem.)
