[Solved]: Relationship between formal system and formal languages

Problem Detail: 

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?

Asked By : Rafael Castro

Answered By : Thomas Klimpel

In my opinion, a formal system should have

1. A well defined set of symbols.
2. A well defined grammar, which tells how well-formed formulas are constructed out of the symbols.
3. One or more well defined inference calculi, which might work similar to the inference calculus associated with a grammar.
4. One or more semantics, allowing to assign meaning to the formulas, propositions and statements of the formal system.

Even so the last point might be contested, it is the one which is responsible for the significant difference between a formal system, and a grammar or a formal language. The inference calculus of a formal system might indeed coincide with the calculus of some grammar, even so it won't normally coincide with the calculus of the grammar of the formal system itself.

(Even a grammar can have multiple inference calculi, but using multiple inference calculi for one formal system is more common in logic, where you want to prove things like cut elimination, or use one formal system as basis for a hierarchy of formal systems.)

A formal language is associated to both a grammar and a formal system. For a formal system, both the set of well-formed formulas, and the set of valid well-formed formulas are formal languages. The formal language is a sort of equivalence resulting from ignoring additional structure like the semantics of the inference calculus, or the finer parts of a grammar. It is one obvious link between formal systems and grammars, but formal systems and grammars can be closer related than expressible by a formal language alone (i.e. they can have an equivalent inference calculus).

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/42443