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.

StackExchange Computer Science Q#42443, answer score: 5