Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation.
For example, an interpretation function could take the predicate T (for "tall") and assign it the extension {a} (for "Abraham Lincoln").
All our interpretation does is assign the extension {a} to the non-logical constant T, and does not make a claim about whether T is to stand for tall and 'a' for Abraham Lincoln.
Though we may take these symbols to stand for certain things or concepts, this is not determined by the interpretation function.
An interpretation often (but not always) provides a way to determine the truth values of sentences in a language.
The essential feature of a formal language is that its syntax can be defined without reference to interpretation.
Many of the commonly studied interpretations associate each sentence in a formal language with a single truth value, either True or False.
The first two columns show the truth-values of the sentence letters as determined by the four possible interpretations.
If our interpretation function makes Φ True, then ¬Φ is made False by the negation connective.
Now the only other possible interpretation of Φ makes it False, and if so, ¬Φ is made True by the negation function.
To make the formal language precise, a specific set of propositional symbols must be fixed.
The standard kind of interpretation in this setting is a function that maps each propositional symbol to one of the truth values true and false.
This extended interpretation is defined inductively, using the truth-table definitions of the logical connectives discussed above.
In the case of function and predicate symbols, a natural number arity is also assigned.
Given a signature σ, the corresponding formal language is known as the set of σ-formulas.
The formal definition of the set of σ-formulas proceeds in the other direction: first, terms are assembled from the constant and function symbols together with the variables.
To ascribe meaning to all sentences of a first-order language, the following information is needed.
An object carrying this information is known as a structure (of signature σ), or σ-structure, or L-structure (of language L), or as a "model".
The truth value of an arbitrary sentence is then defined inductively using the T-schema, which is a definition of first-order semantics developed by Alfred Tarski.
The first is to pass to a larger language in which each element of the domain is named by a constant symbol.
The second is to add to the interpretation a function that assigns each variable to an element of the domain.
The interpretation of a propositional variable is one of the two truth values true and false.
of L: As stated above, a first-order interpretation is usually required to specify a nonempty set as the domain of discourse.
Thus the proof theory of first-order logic becomes more complicated when empty structures are permitted.
Function and relation symbols, in addition to having arities, are specified so that each of their arguments must come from a certain sort.
The intended interpretation of this language has the point variables range over all points on the Euclidean plane, the line variable range over all lines on the plane, and the incidence relation E(p,l) holds if and only if point p is on line l. A formal language for higher-order predicate logic looks much the same as a formal language for first-order logic.
The intended interpretation is called the standard model (a term introduced by Abraham Robinson in 1960).
There are also non-standard models of the (first-order version of the) Peano axioms, which contain elements not correlated with any natural number.
All models are interpretations that have the same domain of discourse as the intended one, but other assignments for non-logical constants.
"[9][failed verification] There are other uses of the term "interpretation" that are commonly used, which do not refer to the assignment of meanings to formal languages.