View source for Syntactic language

A language intended for the study of a formal language while disregarding its main interpretation. The concept of a syntactic language arose in mathematical logic in connection with questions of formalizing and investigating meaningful mathematical theories. The result of formalizing some theory is a [[Formal system|formal system]], which can be regarded as an independent object of study regardless of its origin. A syntactic language is used to study this aspect of formal systems.

A syntactic language is used to describe the language of a formal system — that is, its input symbols, terms, formulas, etc. —, to define the notion of a deduction in the formal system and to formulate and prove theorems about the formal system. Thus, with a formal system, two languages are connected: one is the research language of the formal system itself (the object language) and the other is that in which the formal system is investigated (the syntactic language or meta-language).

A syntactic language must contain names for the symbols and formulas of the object language, and also variables whose values are these symbols and formulas. The symbols and formulas of the object language appear in the syntactic language as their proper names (that is, as the names denoting these symbols and formulas). As a rule, a syntactic language does not have to contain the linguistic machinery for handling infinite sets as independent objects. To emphasize this point, one talks of the elementary syntax of a given formal system, in contrast to the theoretical syntax, in which it is assumed that arbitrary formations can be studied. A language for theoretical syntax is also called a [[Meta-language|meta-language]]. A sufficiently clearly stated syntactic language may be formalized and so become an object language. Many sufficiently strong formal systems can serve as formalizations of their own elementary syntactic language. The proof of the [[Gödel incompleteness theorem|Gödel incompleteness theorem]] for formal systems is based on this fact.

In languages of a theoretical syntax one can consider models of a given formal system and talk about the truth of the formulas of the formal system in these models. An example of a formal language of the theoretical syntax for elementary arithmetic is the second-order language of arithmetic.

====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A. Church,   "Introduction to mathematical logic" , '''1''' , Princeton Univ. Press  (1956)</TD></TR></table>