formal semantics the study of the interpretations of formal languages. A formal language can be defined apart from any interpretation of it. This is done by specifying a set of its symbols and a set of formation rules that determine which strings of symbols are grammatical or well formed. When rules of inference (transformation rules) are added and/or certain sentences are designated as axioms a logical system (also known as a logistic system) is formed. An interpretation of a formal language is (roughly) an assignment of meanings to its symbols and truth conditions to its sentences.
Typically a distinction is made between a standard interpretation of a formal language and a non-standard interpretation. Consider a formal language in which arithmetic is formulable. In addition to the symbols of logic (variables, quantifiers, brackets, and connectives), this language will contain ‘0’, ‘!’, ‘•’, and ‘s’. A standard interpretation of it assigns the set of natural numbers as the domain of discourse, zero to ‘0’, addition to ‘!’, multiplication to ‘•’, and the successor function to ‘s’. Other standard interpretations are isomorphic to the one just given. In particular, standard interpretations are numeral-complete in that they correlate the numerals one-to-one with the domain elements. A result due to Gödel and Rosser is that there are universal quantifications (x)A(x) that are not deducible from the Peano axioms (if those axioms are consistent) even though each A(n) is provable. The Peano axioms (if consistent) are true on each standard interpretation. Thus each A(n) is true on such an interpretation. Thus (x)A(x) is true on such an interpretation since a standard interpretation is numeral-complete. However, there are non-standard interpretations that do not correlate the numerals one-to-one with domain elements. On some of these interpretations each A(n) is true but (x)A(x) is false. In constructing and interpreting a formal language we use a language already known to us, say, English. English then becomes our metalanguage, which we use to talk about the formal language, which is our object language. Theorems proven within the object language must be distinguished from those proven in the metalanguage. The latter are metatheorems. One goal of a semantical theory of a formal language is to characterize the consequence relation as expressed in that language and prove semantical metatheorems about that relation. A sentence S is said to be a consequence of a set of sentences K provided S is true on every interpretation on which each sentence in K is true. This notion has to be kept distinct from the notion of deduction. The latter concept can be defined only by reference to a logical system associated with a formal language. Consequence, however, can be characterized independently of a logical system, as was just done. See also DEDUCTION , LOGICAL SYNTAX, METALANGUAGE , PROOF THEORY , TRANSFOR – MATION RUL. C.S.