Formalized language

An artificial language for which there is a precise formal definition of the class of expressions in the language (and (an interpretation) of the meaning or sense of these expressions). Usually, the expressions of a formalized language are formal combinations of some initial symbols, formed by definite rules of formation of expressions in the given language. The description of the expressions of a formalized language and the connections between them constitute the syntax of the language. The exposition of the meaning of the expressions has to do with the semantics of the language. Thus, to give a formalized language is a matter of constructing its syntax and indicating its semantics. In formulating syntactic concepts of a formalized language one is not allowed to use semantic concepts. All syntactic definitions must be understood by a person unacquainted with the semantics of the language. This basic requirement, which distinguishes formalized languages from natural ones, leads to the separation of syntax from semantics and to the appearance of languages with an identical syntax but different semantics. By a formalized language one often means just its syntax, and the possible semantics are called interpretations of the language.

The clear-cut fixing of linguistic means of expression that can be achieved in a formalized language enables one to eliminate vague references to intuitive obviousness, which are inevitable in the informal axiomatic construction of a theory (see Informal axiomatic method). The formalization of a language creates a basis for formalizing the deductive methods of a mathematical theory under investigation. The concept of a formalized language lies at the bottom of Hilbert's concept of a formal system.

Sometimes the concept of a formalized language includes not just its syntax and semantics, but also a specification of the admissible deductive means for obtaining true propositions of the language (that is, it includes the axioms and derivation rules). Concrete examples of formalized languages are given in the articles Axiomatic set theory; Arithmetic, formal; Predicate calculus, and Types, theory of.

From the semantic point of view one can distinguish the following types of linguistic expressions: variables, terms and formulas. With each variable is associated (in a semantic interpretation) a certain domain of its admissible values — the domain of applicability of the variable. If all the variables happen to have the same domain of applicability, then the language is called single-sorted. Otherwise it is multi-sorted. In a multi-sorted language there must be syntactic rules of formation of sorts, also called types. Each variable of such a language has a definite type. The semantic rules must associate with each type $\tau$ some domain $V_\tau$. The variables with type $\tau$ "run through" $V_\tau$.

Terms and formulas may contain parameters, that is, have free entries of variables (see Free variable). From the semantic point of view a term without parameters (a closed term) is, generally speaking, a composite name denoting an object, while a formula without parameters (a closed formula, or proposition) denotes a judgement. A formalized language can have elementary terms, called constants. They belong among the initial symbols of the language.

If there are parameters, terms are name forms and formulas expression forms. This means that for each admissible collection of values of the free variables (parameters), in accordance with the semantics of the language, a name form denotes an object, and an expression form denotes a judgement. Variables are said to belong to or to occur in the terms. A term that is a variable has this variable as its parameter. Terms and formulas the parameters of which are among the variables $x_1,\dots,x_n$ can be regarded as names of functions and predicates, respectively, in $x_1,\dots,x_n$.

Formulas can also be regarded as terms taking particular truth values (cf. Truth value; in the classical case there are two truth values: "true" and "false" ). With this interpretation of formulas, one can restrict oneself when formulating judgements to those that express the equality of terms to one distinguished term denoting "true" .

There are a wide variety of formalized languages satisfying the requirement of effectiveness, which is that the expressions of the language must be finitary objects, and that all its syntactic concepts (terms, formulas and others) must be algorithmically solvable. One sometimes considers languages that do not satisfy the requirement of effectiveness, in that they contain, for example, infinitely long expressions, or use non-finitary objects as initial symbols. (Thus, in studying vector spaces one uses languages whose initial symbols contain all real numbers.)

In the case when the expressions are non-finitary objects it is impossible to consider the rules of formation of the expressions of the language as intuitively-obvious constructions generating new expressions from ones already constructed. It is necessary to specify both the rules themselves and the ways by which they determine the class of expressions. One can, for example, regard these rules as operations on sets of already available "expressions" , and not as constructions generating new expressions. Here a formalized language must be a free object in an appropriate category. A set-theoretic specification is also used, in which non-finitary objects (in particular, expressions) start from some sufficiently rich sets in a set-theoretic universum (called an admissible set). The rules of formation of expressions are regarded as items in an inductive definition that selects from an admissible set a subclass consisting of expressions.

References

[1]	A. Church, "Introduction to mathematical logic" , 1 , Princeton Univ. Press (1956)
[2]	D. Hilbert, P. Bernays, "Grundlagen der Mathematik" , 1–2 , Springer (1968–1970)
[3]	J. Barwise (ed.) , Handbook of mathematical logic , North-Holland (1977)

Comments

One way to specify a formal(ized) language is by means of an automaton, cf. Formal languages and automata. Cf. also Formal language and Formal language, machine-representable.

The notion of a formal language has become the standard tool for relating descriptions of structures and these structures in areas other than mathematics. The most important application areas outside mathematics are logic, linguistics and computer science. In computer science the whole issue on correctness of programs (either in the context of correctness proofs or synthesis of correct programs) presupposes the presence of a theory assigning meanings to programs. In such a theory programs become phrases in a formal language which is interpreted in some suitable domain. Frequently the construction of these domains leads to complex mathematical problems.

In linguistics the quest for a rigid theory for the semantics of natural language has lead to a proliferation of theories, where formal languages are defined in order to represent fragments of natural languages and are subsequently provided with a semantics in a mathematical model. (Cf. also Mathematical linguistics.)

Although this is not stated explicitly in the main article above, it is clear that only interpretations of formal languages are considered in it which obey the principle of compositionality of meaning: the meaning of a compound expression is composed of the meanings of its parts. This principle, which is known in the tradition of philosophy of language also under the name of Frege's principle, is generally taking as starting point for interpreting formal languages. It formed the basis for the foundation for contemporary semantics which was created by R. Montague in his treatment of a fragment of ordinary English. It can be argued that the compositionality principle provides additional structure to both the formal language itself and to its interpretations: the language becomes an algebra (possibly many-sorted), the semantical domain becomes a similar algebra and the mapping assigning meanings to expressions becomes a homomorphism between these two algebras.

References

[a1]	E. Stoy, "Denotational semantics: The Scott–Strachey approach to programming language theory" , M.I.T. (1977)
[a2]	J.W. de Bakker, "Mathematical theory of program correctness" , Prentice-Hall (1980)
[a3]	R.H. Thomason (ed.) , Formal philosophy, selected papers from Richard Montague , Yale Univ. Press (1974)
[a4]	T.M.V. Janssen, "Foundation and applications of Montague grammar" , 1: Philosophy, framework, computer science , CWI (1986)