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 Interpretation
extends 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(σ) subset of 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_σ->ο = 2^(D_σ) because the predicate type (σ) abbreviates the function type σ->ο, and we can identify predicates ρ in 2^(D_σ) with their extension δρ and those sets with their characterisitic functions χ_δρ in Map(D_σ,{True,False}).

Also we can identify (D⁰->D)=D, as well as 2^(D⁰)={Ø,{()}}={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 υ in Σσ->τ, t in T(Σ)=<σ
	Especially
	φ(υ(t1,...,tn))	= φ(υ)(φ(t1),...,φ(tn))	for υ in Σn is a function, t1,...,tn in 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 and Q) = φ(P) and φ(Q), φ(P or Q) = φ(P) or φ(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 in Int(Σ) ¦ I |= F} subset of Int(Σ)
• For a set of formulas A subset of Formula(Σ) it is
  Mod_Σ(A) := {I in Int(Σ) ¦ for all F in A I |= F}
• For finite sets A = {F₁,...,F_n} it is true that
  I |= A if and only if I |= F₁ and ... and F_n

theory

A set of formulas T subset of Formula(Σ) is a theory :<=> T ⊇ C(T) = {F in Formula(Σ) ¦ T |= F} => T section {F in Formula(Σ) ¦ Mod_Σ(F)=Ø} = Ø xor T = Formula(Σ)

theory of a model set

The theory of a set of models M subset of Int(Σ) is T := Theory(M) := {F in Formula(Σ) ¦ for all I in M I |= F} This is the model-theoretic way of defining theories.
=> T is complete, i.e. for all F in Formula(Σ) (F in T xor ¬F in T).

theory of a formula set

The theory represented by the decidable set of formulas A subset of Formula(Σ) is T := Theory(A) := C(A) = {F in 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 in Σn is a function, d1,...,dn in D
	I(p)(d1,...,dn)	<=> J(p)(φ(d1),...,φ(dn))	if p in Σn is a predicate, d1,...,dn in D

The interpretations I:Σ->D, and J:Σ->E are isomorphic if there is an isomorphism φ:D->E, 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

See Also:

Logic.satisfy(orbital.logic.imp.Interpretation, orbital.logic.imp.Formula), Signature, Map, InterpretationBase.EMPTY(Signature), InterpretationBase.unmodifiableInterpretation(Interpretation)

Invariants:

(Σ == null or keySet() subset of Σ) and for all (s,v) in 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() subset of 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 or keySet() subset of Σ) and for all (s,v) in 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 union i2.

See Also:

Setops.union(java.util.Collection,java.util.Collection)

Postconditions:

RES.getClass() == getClass() && this.equals(OLD)