Relationship between formal system and formal languages In a course of computer science it is common to study the hierarchy of formal languages, grammars, automata and Turing machines. I wonder what is the relationship of these objects with formal systems.

For example, lambda calculus is said to be a formal system.  Would its grammar also be considered a formal system?
Generally speaking, a formal system is comprised of


a language distinguishing its well-formed formulas from those strings over that are not well-formed
some kind of semantics that says which formulas are true and which are not
axioms and inference rules which attempt to generate, computationally, exactly those formulas which are true given the semantics.


We can specify the language of well-formed formulas using a grammar, but a grammar is not itself a formal system.