The study of interpretation of formal systems is the branch of mathematical logic that is known as model theory, and the study of deductive systems is the branch that is known as proof theory.
Some authors, including Rudolf Carnap, define the language as the ordered pair <α, A>.
[3] Carnap also requires that each element of α must occur in at least one string in A.
They are synonymous with the set of strings over the alphabet of the formal language that constitute well formed formulas.
This relation is understood in a comprehensive sense such that the primitive sentences of the formal system are taken as directly derivable from the empty set of sentences.
The theorem is a syntactic consequence of all the well formed formulae that precede it in the proof system.
For a well formed formula to qualify as part of a proof, it must result from applying a rule of the deductive apparatus of some formal system to the previous well formed formulae in the proof sequence.
In metalogic, the words use and mention, in both their noun and verb forms, take on a technical sense in order to identify an important distinction.
This distinction is used to clarify the meaning of symbols of formal languages.
[4] However, it was only with the rise of formal languages in the late 19th and early 20th century that investigations into the foundations of logic began to flourish.
In 1904, David Hilbert observed that in investigating the foundations of mathematics that logical notions are presupposed, and therefore a simultaneous account of metalogical and metamathematical principles was required.
Today, metalogic and metamathematics are largely synonymous with each other, and both have been substantially subsumed by mathematical logic in academia.
A possible alternate, less mathematical model may be found in the writings of Charles Sanders Peirce and other semioticians.