Section 2.7: Interpretations Between Theories
Sometimes we want to show that a theory in a language is at least as powerful as a theory in a language . We can do this by “embedding” the theory with language into the theory with language . This is done by translating from to in such a way that the sentences of are translated to the sentences of . In fact, we are going to do just the opposite. The idea is that, given a translation of to , for any model of , there is a structure in with the universe being a subset of (defined by the translation of ), such that any in is true in (with some ) iff the corresponding translation is true in (with the same ). Given this fact, and the fact that the sentences in are exactly those logically implied by , we conclude that the set of sentences true in every (sentences in so-called ) are those that their translations are in (because the translations are true in every model of ). Note, that up to this point, we have not considered the theory itself, and everything is simply based on the translation of into and . So, at this point, we choose a translation of into and such that , or, even better, .
The flow of discussion is reorganized here compared to the text, as we develop the examples a) showing that is as powerful as , and b) defining functions, following the general discussion.
Given a formula , by we mean where is an alphabetical variant of (see Section 2.4) such that all are substitutable for .
An interpretation is a way in which is translated to and . We need to translate each parameter of to the language of , and we need to consider a specific theory because we must ensure that, for example, the translation of specifies a non-empty set, and the translation of a function symbol indeed specifies a function, i.e. there should be a sentence in that says that our translation is indeed a function (in every model of ).
An interpretation of into is a function that assigns to each parameter of a formula of such that the following requirements hold ( is the set of free variables of ).
- , and .
- For an -place predicate symbol , .
- For an -place function symbol , , and .
- For a constant symbol , , and .
1 says that whatever is a model of , defines a non-empty subset of (the universe for our interpretation of ). 2 says that defines an -place relation (which can be further restricted to the universe defined in 1). 3 says that whatever is a model of , defines an -place relation such that its restriction to the universe defined in 1 is a function (the last element is uniquely defined based on the all others). 4 is just a particular case of 3.
Given an interpretation of into , and a model of , we define the structure for as follows.
- , i.e. the set defined in by .
- , i.e. the relation defined in by restricted to .
- iff , i.e. the function on defined in by .
Given an interpretation of into , and a formula of , we define the syntactical translation of into as follows.
For an atomic formula:
- if , then ,
- otherwise, if is the rightmost function symbol in , and starts the segment of , then , where does not occur in , and is the formula obtained from by replacing the segment with .
For any model of and , iff .
This is a good moment to stop for a second and think about what we have so far. If you understand and clearly see the picture of what is going on, it should be obvious for you, why the lemma holds. When we define an interpretation of into , we, essentially, do two thing. First, for any model of , we define a subuniverse of (by ) and all parameters of on this subuniverse, i.e. we define a structure for , so that for every formula of we can verify whether it is satisfied in with some or not. Note that we use the relations defined by to define the subuniverse and a particular interpretation of the parameters of . At the same time, we can instead translate into using the relations defined by in such a way, that every translation claims something in about the points in only (as long as the range of is in ). What the lemma says is that the two methods to verify whether is satisfied coincide.
a) . Then, iff iff (by definition of ) iff , which is just .
b) is atomic and has function symbols with the rightmost function symbol starting the segment . This is the only tricky point to understand, which we show by induction. Then, iff (by definition of satisfaction). Now, by definition of , where is the unique element such that . So, we continue, iff where has function symbols. By induction, iff iff , which is just . This last “iff” follows from the fact that is the unique element in such that .
c) iff iff iff iff .
d) iff or iff or iff iff .
e) iff for every , iff for every , iff for every , iff iff .
Given the lemma, we can now introduce the largest theory of such that the interpretation of every sentence in the theory is in .
We define the set of -sentences as follows, .
An interpretation of into is an interpretation of into such that .
- Alternatively, it just means that .
An interpretation of into is called a faithful interpretation iff .
- Alternatively, this means that .
- If is complete and is satisfiable, then any interpretation of into is faithful.
If , then there is the identity interpretation of into such that , , and . Accordingly, for every model of , , , , and , i.e. . is an interpretation of into iff .
We want to show that the theory of is as powerful as the theory of . For this, we want to find an interpretation of the theory of into the theory of .
- . We want to find a formula such that for every model of the theory of , it will define as the subset of non-negative integers. But we only have and to define the subset. If it was the set of real numbers, we could have used something like to define it. But for the set of integers we need to use something else. It is known (the Lagrange’s theorem) that an integer number is non-negative iff it is a sum of four squares. Hence, we can use the following formula, . Note, that iff (here, means a non-negative integer number in our particular structure ).
- . This has to be defined as a -place relation. Consider . In , iff .
- . This -place function symbol has to be defined as a -place relation. Consider . In other words, we just say that for every number assigned, if it is one, then plus this number is equal to . Alternatively, it seems, we could have used , which says there exists and .
Then, is a faithful interpretation of into . Indeed, , and iff iff .
...definitions are unlike theorems and unlike axioms. Unlike theorems, definitions are not things we prove... unlike axioms, we do not expect definitions to add substantive information. A definition is expected to add to our convenience, not to our knowledge.
Consider a theory not yet containing the 1-place function symbol . Let where is a wff (not containing ), in which only and may occur free. Then, the following are equivalent:
(a) (the definition is non-creative) For every not containing , if , then .
(b) ( is well-defined) The sentence is in (see Exercise 21 of Section 2.2 for the meaning of the quantifier), i.e. .
Here the idea is that we want to show that the original theory in the language is as powerful as the theory in the augmented language . In other words, definitions do not create additional knowledge.
The interpretation of into we consider is which is the identity interpretation for all parameters except , where . Then, ensures that is indeed an interpretation. Moreover, for every model of , by definition, is the structure of where for every , for the unique such that .
Now, iff is true in for every model of iff is true in for every model of iff . Hence, is a faithful interpretation of into .
Additionally, we can show that the definition is eliminable.
(b) iff .
(c) If does not contain , then .