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?

• I'm asking if a formal grammar can be categorized as a formal system. English is not my usual language, so probably my sentence could be better written. Feel free to rewrite it, if you want to. – Rafael Castro May 14 '15 at 12:58
• Well, I would have edited if it was clear to me what you meant. But OK, I tried editing with one possible guess at what you might have meant. Does the edit represent what you were trying to ask? – D.W. May 15 '15 at 6:05

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).

• There is any reference about this subject ? I would appreciate to read a text that discuss this. – Rafael Castro May 12 '15 at 0:40
• I like the Stanford Encyclopedia of Philosophy, for example plato.stanford.edu/entries/goedel-incompleteness, plato.stanford.edu/entries/hilbert-program or plato.stanford.edu/entries/frege. But you could also lookup "formal system" in a normal encyclopedia, like wikipedia or Encyclopædia Britannica. Usage of formal systems will come up in universal algebra (equational logic, and quasi-equational logic), logic (propositional calculus, predicate calculus, modal logic), in computer science (automata and formal languages), ... – Thomas Klimpel May 13 '15 at 16:23

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.

A formal language $\mathcal{L}$ is composed of:

• an alphabet of symbols, that is a set of symbols with the particularity that each of those symbols can be specified without reference to any interpretation. The alphabet of a formal language $\mathcal{L}$ is often referred as $\Sigma$.

• a grammar that determines which sequences of symbols in $\Sigma$ are well-defined-formulas (often called wffs) in $\mathcal{L}$.

A formal system $\mathcal{S}$ is:

• A formal language $\mathcal{L}$
• A deductive apparatus.

What is a deductive apparatus you may ask?

• An arbitrary set of wffs in $\mathcal{L}$ that are axioms

• A set of inference rules that determines which wffs have a relation of "immediate consequence" between them.

Here are a some excellent references whether you want to get started or dive into more meaty stuff:

• Metalogic: An Introduction to the metatheory of Standard First Order Logic by Geoffrey Hunter.

• Automata, Formal Languages and Algebraic Systems by Masami Ito

What you see in an introductory course in formal languages is just a small sample of the multitude of models used to define and study languages (or functions, numbers, etc.) formally, i.e., regarding their syntactical structure - that has a dynamic component, which we call "computation" -, setting aside what could be considered their content, to be "reattached" to these structures a posteriori, or not at all. These different models come from different contexts and have different applications, theoretical as well as practical.

The language used to describe these models can also be formalized, so you have grammars both as formal systems and as languages. This kind of circularity is problematic, but unavoidable, and in many cases desirable.

The notion of formal system as it is used in computer science has to do historically with the investigation of formal properties of mathematical logic systems. The standard definitions you will see in other answers come from this common origin. There are other kinds of formal systems in other fields of research, the term is polysemic. The distinction between concepts of form and content depends on where you're coming from.

I'm looking for the same question, and seems there are no clarity. I hope someone could give us.

See, for instance, what Levelt state in his book ("An Introduction to the Theory of Formal Languages and Automata" Cap1, p. 1):

From a mathematical point of view, grammars are FORMAL SYSTEMS, like Turing machines, computer programs, prepositional logic, theories of inference, neural nets, and so forth. 

Despite of this, it's a really matter whats others answers pointed out here, because formal grammars seems truly miss some fundamental attributes (i.e. deductive apparatus) to be marked as formal systems.

However, if a Turing machine is a formal system , and formal languages (and its representations, grammars) are equivalents to them: why grammars is not a formal system too?

I hope this consideration, event though are not conclusive may animate some improved answer to this problem.