Orbital library

## orbital.logic.imp Interface Interpretation

Type Parameters:
`Sigma` - the type of symbols kept in this interpretation.
`Denotation` - the type of denotating objects.
All Superinterfaces:
java.util.Map
All Known Implementing Classes:
InterpretationBase

`public interface Interpretationextends java.util.Map`

An interpretation associates the symbols in a signature with the entities in the world (for semantics). The arbitrary symbols in the signature are given a meaning with an interpretation, only.

In principle, semantics of syntactic expressions are usually defined with denotational semantics for interpretations, with operational semantics for a calculus, and sometimes with algebraic semantics or logical semantics.

A (denotational) interpretation is a mapping from signs to referents. More precisely

interpretation
an interpretation I:Σ→D is a family of maps I:ΣτDτ for each type τ, with
• I maps symbols of `type` τ to elements of the class I(τ):=Dτ ≠ ∅. Especially in computer science, the class I(τ) is often assumed to be a set, even though this is rather irrelevant. "Wilfrid Hodges. Elementary Predicate Logic. In: Dov M. Gabbay and F. Guenther. Handbook of philosophical logic Volume 1 2nd edition. paragraph 17 theorem 10"
• I respects subtypes: for types στ the sets satisfy I(σ)⊆I(τ).
• Dο is the set of truth-values for the type ο = () of truth-values (also the type of atomic formulas). For two-valued logics this means Dο := Boole := {True,False}.
• Dι := D is a set called universe or domain of I for the type ι of individuals. It is non-empty by presupposition of existence.
• Dσ→τ := Map(Dσ,Dτ) = DτDσ.
• D(σ) = Dσ→ο ≅ ℘(Dσ) because the predicate type (σ) abbreviates the function type σ→ο, and we can identify predicates ρ∈℘(Dσ) with their extension δρ and those sets with their characterisitic functions χδρ∈Map(Dσ,{True,False}).
Also we can identify (D0D)≅D, as well as ℘(D0)={∅,{()}}≅{True,False}. Interpretations are homomorphisms.
homomorphism
 φ:T(Σ)→D is a homomorphism of (typed) Σ-algebras, i.e. a family of maps φ:T(Σ)τ→Dτ, if φ(υ(t)) = φ(υ)(φ(t)) for υ∈Σσ→τ, t∈T(Σ)≤σ Especially φ(υ(t1,…,tn)) = φ(υ)(φ(t1),…,φ(tn)) for υ∈Σn is a function, t1,…,tn∈T(Σ)
truth-functional
If for every interpretation I:Σ→D there is a unique continuation φ:T(Σ)→D that is a homomorphism of Σ-algebras, i.e.
φ|Σ = I and φ is homomorphic
Then the logic is called truth-functional, and that unique homomorphism φ is called the (expression) valuation or truth-function, which is again denoted by I.
"Evaluations are the homomorphic continuation of symbol interpretations."
Note that the homomorphism conditions for φ include
φ(¬P) = ¬φ(P), φ(P∧Q) = φ(P)∧φ(Q), φ(P∨Q) = φ(P)∨φ(Q), φ(P→Q) = φ(P)→φ(Q) etc.

If a logic is truth-functional, the semantics of a combined formula can be defined with the combined semantics of the components and junctors. Then the junctors are treated truth-functionally, that is, every junctor is defined by its corresponding function that maps the combined truth-values to resulting truth-values. This is denoted with truth-tables.

If we have a truth-functional logic, we can define the satisfaction relation with truth-functions

I ⊧ F :⇔ I(F) = true
The satisfaction relation defines the semantics of a formula. In effect, it encapsulates the details of truth-functions into a single relation. Although this may not instantly appear to be of advantage, we then receive the freedom of interchanging the satisfaction relation (or even any truth-functions underlying it).

An interpretation I is a satisfying Σ-Model of F, if:

I ⊧ F, i.e. the interpretation satisfies the formula.
• The set of all satisfying Σ-Models of F is
ModΣ(F) := {I∈Int(Σ) ¦ I ⊧ F} ⊆ Int(Σ)
• For a set of formulas A⊆Formula(Σ) it is
ModΣ(A) := {I∈Int(Σ) ¦ for all F∈A I ⊧ F}
• For finite sets A = {F1,…,Fn} it is true that
I ⊧ A if and only if I ⊧ F1∧…∧Fn

theory
A set of formulas T⊆Formula(Σ) is a theory :⇔
TC(T) = {F∈Formula(Σ) ¦ T F}
T∩{F∈Formula(Σ) ¦ ModΣ(F)=∅} = ∅ xor T = Formula(Σ)
theory of a model set
The theory of a set of models M⊆Int(Σ) is
T := Theory(M) := {F∈Formula(Σ) ¦ ∀I∈M I ⊧ F}
This is the model-theoretic way of defining theories.
T is complete, i.e. ∀F∈Formula(Σ) (F∈T xor ¬F∈T).
theory of a formula set
The theory represented by the decidable set of formulas A⊆Formula(Σ) is
T := Theory(A) := C(A) = {F∈Formula(Σ) ¦ A F} = Theory(Mod(A))
A is called the presentation or axiomatization of the theory T which is said to be axiomatizable. The definition as consequence closure is the axiomatic way of defining theories.
T is semi-decidable.

In addition to this syntactic aspect, theories, when applied to a particular domain, should just as well explain observed facts.

Now we consider possible equivalence relations of interpretations.

elementary equivalent
Two interpretations I:Σ→D, and J:Σ→E are elementary equivalent, iff
Theory({I}) = Theory({J})
i.e. they satisfy the same formulas of the logic L.
homomorphism
Let I:Σ→D, J:Σ→E be two interpretations.
 φ:D→E is a homomorphism of interpretations, if φ(I(f)(d1,…,dn)) = J(f)(φ(d1),…,φ(dn)) if f∈Σn is a function, d1,…,dn∈D I(p)(d1,…,dn) ⇔ J(p)(φ(d1),…,φ(dn)) if p∈Σn is a predicate, d1,…,dn∈D
The interpretations I:Σ→D, and J:Σ→E are isomorphic if there is an isomorphism φ:DE, i.e. a bijective homomorphism. Isomorphic interpretations are elementary equivalent.

An interpretation associates each sign in the signature Σ with an object value, its interpretation. Especially, our interpretations include valuations (variable assignments). Valuations are a technique introduced by Tarski, for dealing with the semantics of quantifiers.

Author:
André Platzer
`Logic.satisfy(orbital.logic.imp.Interpretation, orbital.logic.imp.Formula)`, `Signature`, `Map`, `InterpretationBase.EMPTY(Signature)`, `InterpretationBase.unmodifiableInterpretation(Interpretation)`
Invariants:
(Σ == null ∨ keySet() ⊆ Σ) ∧ ∀(s,v)∈this s.getType().apply(v)
Structure:
extends java.util.Map
Note:
This interface could be strengthened by extending SortedMap instead of just Map.

Nested Class Summary

Nested classes/interfaces inherited from interface java.util.Map
`java.util.Map.Entry`

Method Summary
` boolean` `containsKey(java.lang.Object symbol)`
Returns whether the specified symbol is contained in this interpretation assocation map.
` boolean` `equals(java.lang.Object o)`
Checks two interpretations for extensional equality.
` java.lang.Object` `get(java.lang.Object symbol)`
Get the referent associated with the given symbol in this interpretation.
` Signature` `getSignature()`
Get the signature interpreted.
` int` `hashCode()`
Get a hash code fitting extensional equality.
` java.lang.Object` ```put(java.lang.Object symbol, java.lang.Object referent)```
Set the referent associated with the given symbol in this interpretation.
` void` `putAll(java.util.Map associations)`
Copies all of the associations from the specified map to this interpretation.
` void` `setSignature(Signature sigma)`
Set the signature interpreted.
` Interpretation` `union(Interpretation i2)`
Returns the union of two interpretations.

Methods inherited from interface java.util.Map
`clear, containsValue, entrySet, isEmpty, keySet, remove, size, values`

Method Detail

### equals

`boolean equals(java.lang.Object o)`
Checks two interpretations for extensional equality. Two interpretations are equal if both their signatures and interpretation objects are equal.

Specified by:
`equals` in interface `java.util.Map`
Overrides:
`equals` in class `java.lang.Object`

### hashCode

`int hashCode()`
Get a hash code fitting extensional equality. .

Specified by:
`hashCode` in interface `java.util.Map`
Overrides:
`hashCode` in class `java.lang.Object`

### getSignature

`Signature getSignature()`
Get the signature interpreted.

### setSignature

`void setSignature(Signature sigma)`
Set the signature interpreted.

Throws:
`java.lang.IllegalArgumentException` - if sigma does not contain a symbol which is interpreted in the current assocation map. This is not checked if sigma is `null`.
Preconditions:
sigma == null || keySet() ⊆ sigma

### get

`java.lang.Object get(java.lang.Object symbol)`
Get the referent associated with the given symbol in this interpretation.

Overwrite along with other map operations like `Set.contains(Object)` to implement a different source for symbol associations.

Specified by:
`get` in interface `java.util.Map`
Throws:
`java.util.NoSuchElementException` - if the symbol is not in the current signature Σ.
Postconditions:
symbol.getType().apply(RES)

### put

```java.lang.Object put(java.lang.Object symbol,
java.lang.Object referent)```
Set the referent associated with the given symbol in this interpretation.

Specified by:
`put` in interface `java.util.Map`
Throws:
`java.util.NoSuchElementException` - if the symbol is not in the current signature Σ.
`TypeException` - if the referent is not of the type of symbol.
Preconditions:
symbol.getType().apply(referent)

### putAll

`void putAll(java.util.Map associations)`
Copies all of the associations from the specified map to this interpretation.

Specified by:
`putAll` in interface `java.util.Map`
Throws:
`java.lang.IllegalArgumentException` - if associations does contain a symbol which is not contained in the signature. This is not checked if Σ is `null`.
`TypeException` - if one of the values is not of the type of its symbol.
`java.lang.NullPointerException` - if associations is `null`.
Preconditions:
(Σ == null ∨ keySet() ⊆ Σ) ∧ ∀(s,v)∈associations

### containsKey

`boolean containsKey(java.lang.Object symbol)`
Returns whether the specified symbol is contained in this interpretation assocation map.

Specified by:
`containsKey` in interface `java.util.Map`
Throws:
`java.util.NoSuchElementException` - if the symbol is not in the current signature Σ.

### union

`Interpretation union(Interpretation i2)`
Returns the union of two interpretations.

Parameters:
`i2` - the interpretation to merge with this one, resulting in a new interpretation. (If a symbol is contained in both interpretations, the value of i2 will precede over the value of this.)
Returns:
i ∪ i2.
`Setops.union(java.util.Collection,java.util.Collection)`