Interpretatibility 2

arity separates the syntactically undifferentiated constants of L into n-place predicates, n-place function symbols, and individual constants. This partitioning of the constants explicitly reflects the intuitive ontology of traditional first-order logic expressed in its semantics – relations, functions, and individuals. We can reflect the same ontology despite CL's undifferentiated constants, however, simply by introducing appropriate predicates and interpreting them in a way that parallels the semantics of traditional first-order logic.

Specifically, we define the CL language L⁺ obtained from L by the addition of denumerably many new constants Rel-0, Rel-1, …, Fn-0, Fn-1, …, and a new constant Ind. (We assume without any loss of generality that L did not contain these constants to begin with.) Let I = 〈D,ext,skol,V〉 be an L₁-agreeable interpretation of L, where D = A ∪ R). Say that and interpretation I⁺ = 〈D⁺,ext⁺,skol⁺,V⁺〉 of L⁺ is a CL reflection of I if

D = A ∪ R⁺ and R ⊆ R⁺;
ext ⊆ ext⁺;
skol ⊆ skol⁺;
V ⊆ V⁺;
V⁺ maps all of the new constants one-to-one into R⁺ - R;
ext⁺(V⁺(Rel-n)) = {V(π) : p-arity(π) = n};
ext⁺(V⁺(Fn-n)) = {V(π) : f-arity(π) = n};
ext⁺(V⁺(Ind)) = A.

We now define a syntactic function * that maps each sentence φ of L₁ to a sentence φ* of L⁺ such that, intuitively, for any L₁-agreeable interpretation I of L, φ means the same thing in I that φ* does in any CL reflection of I. The definition is obvious enough:

If κ is an individual constant or variable, then κ* is κ; If (π τ₁ ... τ_n)* = (and (Rel-n π) (Ind τ₁) … (Ind τ_n) (π τ₁ ... τ_n) there is a certain theory Γ expressed in an extension L⁺ of L and a mapping * from L₁ into L⁺ such that for any formula φ of L, and any L₁-agreeable interpretation I, φ is true₁ in I iff φ* is true in I.
The language L⁺ of the theory Γ extends L with the addition of a constant Ind and countably many contants Rel-0, Rel-1, ….
```
(<=> (Ind ?x) (not (Rel-n ?x))), for any n.
```
```
(=> (π τ₁ ... τ_n)
    (and (Rel-n π)
         (Ind τ₁) … (Ind τ_n)))
```
If n ≠ m, then every instance of the following two schemas is an axiom:
```
(=> (π τ₁ ... τ_n)
    (not (π σ₁ ... σ_m)))
```
```
(⇒ (Rel-n ?x)
    (not (Rel-m ?x)))
```
Christopher Menzel
Last modified: Sun Nov 17 12:06:47 CST 2002