# Interpretation Representation and Model Verification

by Geoff Sutcliffe, Alex Steen, Pascal Fontaine

## Representation of FOF Finite Interpretations

Consider the following FOF problem from the
TPTP Format for Finite Interpretations in the TPTP Quick Guide. It is CounterSatisfiable, i.e., there is a model for the axioms and negated conjecture.
```%------------------------------------------------------------------------------
%----All (hu)men are created equal. John is a human. John got an F grade.
%----There is someone (a human) who got an A grade. An A grade is not
%----equal to an F grade. Grades are not human. Therefore, it is not the
%----case being created equal is the same as really being equal.

fof(all_created_equal,axiom,
! [H1,H2] :
( ( human(H1)
& human(H2) )
=> created_equal(H1,H2) ) ).

fof(john,axiom,
human(john) ).

fof(john_failed,axiom,
grade(john) = f ).

fof(someone_got_an_a,axiom,
? [H] :
( human(H)
& grade(H) = a ) ).

a != f ).

! [G] : ~ human(grade(G)) ).

fof(equality_lost,conjecture,
! [H1,H2] :
( ( human(H1)
& human(H2)
& created_equal(H1,H2) )
<=> H1 = H2 ) ).

%------------------------------------------------------------------------------

```
A weakness of the format for the finite interpretation presented in the TPTP Format for Finite Interpretations in the TPTP Quick Guide is that the format relies on the formulae names (all the same) to link the three components of the interpretation, which is not allowed in the TPTP world. How about merging them to, e.g., ...
```%------------------------------------------------------------------------------
fof(equality_lost,interpretation,
( ! [X] : ( X = "a" | X = "f" | X = "john" | X = "gotA")
& ( a = "a"
& f = "f"
& john = "john"
& grade("a") = "a"
& grade("f") = "a"
& grade("john") = "f"
& grade("gotA") = "a" )
& ( ~ human("a")
& ~ human("f")
& human("john")
& human("gotA")
& ~ created_equal("a","a")
& ~ created_equal("a","f")
& ~ created_equal("a","john")
& ~ created_equal("a","gotA")
& ~ created_equal("f","a")
& ~ created_equal("f","f")
& ~ created_equal("f","john")
& ~ created_equal("f","gotA")
& ~ created_equal("john","a")
& ~ created_equal("john","f")
& created_equal("john","john")
& created_equal("john","gotA")
& ~ created_equal("gotA","a")
& ~ created_equal("gotA","f")
& created_equal("gotA","john")
& created_equal("gotA","gotA") ) ) ).

%------------------------------------------------------------------------------

```
Note how the use of "distinct object"s makes the domain elements distinct.

FOF_Finite.s.p is the proof problem to verify the (counter) model using the technique discussed in Verification of Models.

## Representation of TFF/TXF Interpretations

The example of a finite FOF interpretation clearly points to the need for types. The problem would be better written as ...
```%------------------------------------------------------------------------------
%----All (hu)men are created equal. John is a human. John got an F grade.
%----There is someone (a human) who got an A grade. An A grade is not
%----equal to an F grade. Grades are not human. Therefore, it is (actually
%----not) the case being created equal is the same as really being equal.
tff(man_type,type,           man: \$tType ).
tff(john_decl,type,          john: man ).
tff(a_decl,type,             a: grade ).
tff(f_decl,type,             f: grade ).
tff(created_equal_decl,type, created_equal: ( man * man ) > \$o ).

tff(all_created_equal,axiom,
! [H1: man,H2: man] : created_equal(H1,H2) ).
tff(john_failed,axiom,
grade_of(john) = f ).
tff(someone_got_an_a,axiom,
? [H: man] : grade_of(H) = a ).
a != f ).
tff(equality_lost,conjecture,
! [H1: man,H2: man] :
( created_equal(H1,H2)
<=> ( H1 = H2 ) ) ).

%------------------------------------------------------------------------------

```
... and a finite interpretation (a countermodel for the conjecture) is ...
```%------------------------------------------------------------------------------
tff(man_type,type,           man: \$tType ).
tff(john_decl,type,          john: man ).
tff(a_decl,type,             a: grade ).
tff(f_decl,type,             f: grade ).
tff(created_equal_decl,type, created_equal: ( man * man ) > \$o ).

tff(d_man_type,type,         d_man: \$tType).
tff(d_to_man_decl,type,      d_to_man: d_man > man ).

tff(d_john_decl,type,        d_john: d_man ).
tff(d_got_A_decl,type,       d_got_A: d_man ).
tff(d_a_decl,type,           d_a: d_grade ).
tff(d_f_decl,type,           d_f: d_grade ).

tff(equality_lost,interpretation,
%----The two man domain elements are d_john and d_got_A
( ! [X: d_man] : ( X = d_john | X = d_got_A )
& \$distinct(d_john,d_got_A)
%----The type promoter is a bijection (injective and surjective)
& ! [X: d_man,Y: d_man] : ( d_to_man(X) = d_to_man(Y) => X = Y )
& ! [X: man] : ? [DX: d_man] : d_to_man(DX) = X
%----The two grade domain elements are d_a and d_f
& ! [X: d_grade]: ( X = d_a | X = d_f )
& \$distinct(d_a,d_f)
%----The type promoter is a bijection (injective and surjective)
& ! [X: d_grade,Y: d_grade] : ( d_to_grade(X) = d_to_grade(Y) => X = Y )
& ! [X: grade] : ? [DX: d_grade] : d_to_grade(DX) = X
%----Interpret terms via the type-promoted domain elements
& ( a = d_to_grade(d_a)
& f = d_to_grade(d_f)
& john = d_to_man(d_john)
%----Interpret atoms as true of false
& ( created_equal(d_to_man(d_john),d_to_man(d_john))
& created_equal(d_to_man(d_john),d_to_man(d_got_A))
& created_equal(d_to_man(d_got_A),d_to_man(d_john))
& created_equal(d_to_man(d_got_A),d_to_man(d_got_A)) ) ) ).
%----To clarify, if John was not equal to the man who got an A, it would be
%----     & ~ created_equal(d_to_man(d_john),d_to_man(d_got_A))
%----     & ~ created_equal(d_to_man(d_got_A),d_to_man(d_john))

%------------------------------------------------------------------------------

```
Hmmm, should the types be inside the interpretation?

TFF_Finite.s.p is the proof problem to verify the (counter) model using the technique discussed in Verification of Models.

## Representation of Infinite Interpretations

I'm just spitballing here, but I don't see any problem with relaxing the format for finite interpretations to allow infinite interpretations, with domains of integer size or even real size. Consider the following TFF example that requires an integer size model ...
```%------------------------------------------------------------------------------
tff(person_type,type,        person: \$tType ).
tff(bob_decl,type,           bob: person ).
tff(child_of_decl,type,      child_of: person > person ).
tff(is_descendant_decl,type, is_descendant: ( person * person ) > \$o ).

tff(descendents_different,axiom,
! [A: person,D: person] : ( is_descendant(A,D) => ( A != D ) ) ).
tff(descendent_transitive,axiom,
! [A: person,C: person,G: person] :
( ( is_descendant(A,C) & is_descendant(C,G) ) => is_descendant(A,G) ) ).
tff(child_is_descendant,axiom,
! [P: person] : is_descendant(P,child_of(P)) ).
tff(all_have_child,axiom,
! [P: person] : ? [C: person] : ( C = child_of(P) ) ).

%------------------------------------------------------------------------------

```
How's this for an explicit infinite model using integers for the domain elements ...
```%------------------------------------------------------------------------------
tff(person_type,type,        person: \$tType ).
tff(bob_decl,type,           bob: person ).
tff(child_of_decl,type,      child_of: person > person ).
tff(is_descendant_decl,type, is_descendant: ( person * person ) > \$o ).

tff(d_to_person_decl,type,   d_to_person: \$int > person ).

tff(equality_lost,interpretation,
%----The type promoter is a bijection (injective and surjective)
( ! [ID1: \$int,ID2: \$int] : ( d_to_person(ID1) = d_to_person(ID2) => ID1 = ID2 )
& ! [D: person] : ? [ID: \$int] : d_to_person(ID) = D
%----Mapping people to integers
& bob = d_to_person(0)
& ! [N: \$int] :
child_of(d_to_person(N)) = d_to_person(\$sum(N,1))
%----Interpretation of descendancy
& ! [A: \$int,D: \$int] :
( is_descendant(d_to_person(A),d_to_person(D)) <=> \$less(A,D) ) ) ).

%------------------------------------------------------------------------------

```
TFF_Infinite.s.p is the proof problem to verify the (counter) model using the technique discussed in Verification of Models.

## Representation of Finite-Finite Kripke Interpretations

This can be done in only a typed logic.

Record world information in one formula, using a new defined type \$ki_world, a new defined predicate \$in_ki_world with type \$ki_world > \$o, a new defined predicate \$accessible_ki_world with type (\$ki_world * \$ki_world) > \$o, and a new defined constant \$initial_ki_world with type \$ki_world. Syntactically distinct constants of type \$ki_world are known to be unequal. The interpretation in a world is represented as above, with guards used to specify the worlds in which the interpretation is used.

Here's a problem that has a counter model with a finite number of worlds each of which has a finite domain (hence "Finite-Finite Kripke Interpretation") ...

```%------------------------------------------------------------------------------
tff(simple_spec,logic,
\$alethic_modal == [
\$constants == \$rigid,
\$quantification == \$constant,
\$modalities == \$modal_system_T ] ).

tff(fruit_type,type,fruit: \$tType).
tff(apple_decl,type,apple: fruit).
tff(banana_decl,type,banana: fruit).
tff(healthy_decl,type,healthy: fruit > \$o).
tff(rotten_decl,type,rotten: fruit > \$o).

tff(necessary_healthy_fruit_everywhere,axiom,
! [F: fruit] : {\$necessary} @ (healthy(F)) ).

tff(rotten_apple_everywhere,axiom,
rotten(apple) ).

tff(rotten_banana_here,axiom-local,
rotten(banana) ).

tff(not_true,conjecture,
~ ( healthy(apple)
& {\$possible} @ (~ rotten(banana)) ) ).

%------------------------------------------------------------------------------

```
After using NTF2THF to embed the problem into TH0, Nitpick finds this counter model ...
```%------------------------------------------------------------------------------
tff(fruit_type,type,fruit: \$tType).
tff(apple_decl,type,apple: fruit).
tff(banana_decl,type,banana: fruit).
tff(healthy_decl,type,healthy: fruit > \$o).
tff(rotten_decl,type,rotten: fruit > \$o).

tff(w1_decl,type,w1: \$ki_world).
tff(w2_decl,type,w2: \$ki_world).
tff(d_fruit_type,type,d_fruit: \$tType).
tff(d_to_fruit,type, d_to_fruit: d_fruit > fruit )
tff(d_apple_decl,type,d_apple: d_fruit).
tff(d_banana_decl,type,d_banana: d_fruit).

tff(fruity_worlds,interpretation,
( ! [W: \$ki_world] : ( W = w1 | W = w2 )
& \$initial_ki_world = w1
& ( \$accessible_ki_world(w1,w2) )
& ! [W: \$ki_world] : \$accessible_ki_world(W,W)     %----Logic is T
& ( \$in_ki_world(w1)
=> ( ! [X: d_fruit] : ( X = d_apple | X = d_banana )
& \$distinct(d_apple,d_banana)
& ! [X: d_fruit,Y: d_fruit] : ( d_to_fruit(X) = d_to_fruit(Y) => X = Y )
& ! [X: fruit] : ? [DX: d_fruit] : d_to_fruit(DX) = X
& ( apple = d_to_fruit(d_apple)
& banana = d_to_fruit(d_banana) )
& ( healthy(d_to_fruit(d_apple))
& healthy(d_to_fruit(d_banana))
& rotten(d_to_fruit(d_apple))
& rotten(d_to_fruit(d_banana)) ) ) )
& ( \$in_ki_world(w2)
=> ( ! [X: d_fruit] : ( X = d_apple | X = d_banana )
& \$distinct(d_apple,d_banana)
& ! [X: d_fruit,Y: d_fruit] : ( d_to_fruit(X) = d_to_fruit(Y) => X = Y )
& ! [X: fruit] : ? [DX: d_fruit] : d_to_fruit(DX) = X
& ( apple = d_to_fruit(d_apple)
& banana = d_to_fruit(d_banana) )
& ( healthy(d_to_fruit(d_apple))
& healthy(d_to_fruit(d_banana))
& rotten(d_to_fruit(d_apple))
& ~ rotten(d_to_fruit(d_banana)) ) ) )) ).

%----Logic 4, if I wanted it.
% tff(ki_system_4,axiom,
%     ! [W1: \$ki_world,W2: \$ki_world,W3: \$ki_world]
%       ( ( \$accessible_ki_world(W1,W2)
%         & \$accessible_ki_world(W2,W3) )
%      => \$accessible_ki_world(W1,W3) ) ).

%------------------------------------------------------------------------------

```
NTF_Finite-Finite.s.p is the proof problem to verify the (counter) model using the technique discussed in Verification of Models.

## Representation of Finite-Infinite Kripke Interpretations

This example requires (I think) only three worlds, but they have to have infinite domains. The current world has the start "state" null and a sequence of other states using red xor green flips. One of the other two world starts with a red sequence, and the other starts with a green sequence. As sequences with different colours are distinct, the two world need to have different infinite domains. I think.
```%------------------------------------------------------------------------------
tff(simple_spec,logic,
\$alethic_modal == [
\$constants == \$rigid,
\$quantification == \$constant,
\$modalities == \$modal_system_T ] ).

tff(colour_type,type, colour: \$tType ).
tff(sequence_type,type, sequence: \$tType ).

tff(red_decl,type, red: colour ).
tff(green_decl,type, green: colour ).
tff(null_decl,type, null: sequence ).
tff(flip_decl,type, flip: ( colour * sequence ) > sequence ).
tff(state_decl,type, state: sequence > \$o ).

tff(only_two_different_colours,axiom,
! [C: colour] : ( ( C = red ) <~> ( C = green ) ) ).

tff(null_not_flip,axiom,
! [C: colour,S: sequence] : ( null != flip(C,S) ) ).

tff(different_flips_1,axiom,
! [S: sequence] : ( flip(red,S) != flip(green,S) ) ).

tff(different_flips_2,axiom,
! [C: colour,S1: sequence,S2: sequence] :
( ( flip(C,S1) = flip(C,S2) ) => ( S1 = S2 ) ) ).

tff(next_state,axiom,
! [S: sequence] :
( state(S)
=> ( state(flip(red,S)) <~> state(flip(green,S)) ) ) ).

tff(start_state,axiom-local,
state(null)).

tff(possible_states,axiom-local,
! [S: sequence] :
( ( {\$possible} @ (state(flip(red,S))) )
& ( {\$possible} @ (state(flip(green,S))) ) ) ).
%------------------------------------------------------------------------------

```

## Representation of Infinite-Finite Kripke Interpretations

This example requires (I think) an infinite number of worlds. The interpretation in the current world will have an infinite domain, but all the other worlds' domains need only a single element (one of the domain elements from the current world). All the domain elements of the current world need to have a corresponding world with that domain element.
```%------------------------------------------------------------------------------
tff(simple_spec,logic,
\$alethic_modal == [
\$constants == \$flexible,
\$quantification == \$varying,
\$modalities == \$modal_system_T ] ).

tff(person_type,type,person: \$tType).
tff(geoff_decl,type,geoff: person).
tff(like_decl,type,like: person > \$o).
tff(id_of_decl,type,id_of: person > \$int).

%----Infinite people. The RHS of the conjunction limits it to an integer number
%----of people.
tff(infinite_people,axiom-local,
( ! [I: \$int] :
( \$greatereq(I,0)
=> ( ? [P: person] :
id_of(P) = I
& ! [P1: person,P2: person] :
( ( id_of(P1) = id_of(P2) )
=> ( P1 = P2 ) ) ) ) ) ).

tff(like_geoff_and_only_geoff,axiom,
( like(geoff)
& ! [P: person] :
( like(P)
=> P = geoff ) ) ).

tff(like_all,axiom-local,
! [X: person] : {\$possible} @ (like(X)) ).

%------------------------------------------------------------------------------

```
Here's a model with an integer number of worlds.
```%------------------------------------------------------------------------------
tff(person_type,type,person: \$tType).
tff(geoff_decl,type,geoff: person).
tff(like_decl,type,like: person > \$o).
tff(id_of_decl,type,id_of: person > \$int).

tff(d_to_person_decl,type, d_to_person: \$int > person ).
tff(d_id_of_decl,type,id_of: person > \$int).

tff(w_to_ki_world_decl,type,w_to_ki_world: \$int > \$ki_world ).
%----To fool Vampire
tff(ki_world_type,type,\$ki_world: \$tType).
tff(initial_ki_world_decl,type,\$initial_ki_world : \$ki_world).
tff(in_ki_world_decl,type,\$in_ki_world: \$ki_world > \$o).
tff(accessible_ki_world_decl,type,\$accessible_ki_world: (\$ki_world * \$ki_world) > \$o).

tff(ki_name,interpretation,
%----An infinite number of worlds, numbered by naturals
( ! [IW: \$int] :
( \$greatereq(IW,0)
=> ? [W: \$ki_world] : w_to_ki_world(IW) = W )
& \$initial_ki_world = w_to_ki_world(0)
%----The type promoter is a bijection (injective and surjective)
& ! [IW1: \$int,IW2: \$int] : ( ( w_to_ki_world(IW1) = w_to_ki_world(IW2) ) => ( IW1 = IW2 ) )
& ! [W: \$ki_world] : ? [IW: \$int] : w_to_ki_world(IW) = W
%----World 0 can access itself (system T)
& \$accessible_ki_world(w_to_ki_world(0),w_to_ki_world(0))
%----World 0 can access all other worlds
& ! [IW: \$int] :
( \$greater(IW,0)
=> \$accessible_ki_world(w_to_ki_world(0),w_to_ki_world(IW)) )

%----Now interpret each world
%----The type promoter is a bijection (injective and surjective)
& ! [ID1: \$int,ID2: \$int] : ( d_to_person(ID1) = d_to_person(ID2) => ID1 = ID2 )
& ! [D: person] : ? [ID: \$int] : d_to_person(ID) = D
%----In world 0
& ( \$in_ki_world(w_to_ki_world(0))
%----There are infinite domain elements
=> ( ! [P: person] : ? [ID: \$int] : P = d_to_person(ID)
%----geoff is interpreted as 0
& geoff = d_to_person(0)
%----id_of coincides with the domain elements
& ! [I: \$int] : id_of(d_to_person(I)) = I
%----like is true for 0
& like(d_to_person(0) ) ) )
%----In other worlds there is one domain element
& ! [W: \$int] :
( ( \$greater(W,0)
& \$in_ki_world(w_to_ki_world(W)) )
%----There is a domain element for geoff, and that's the only domain element
=> ( ? [GID: \$int] :
( geoff = d_to_person(GID)
& ! [ID: \$int] :
( geoff = d_to_person(ID)
=> ID = GID ) )
%----geoff is interpreted as the same domain element as the world number
& geoff = d_to_person(W)
& id_of(d_to_person(W)) = W
& like(d_to_person(W)) ) ) ) ).

%------------------------------------------------------------------------------

```

## Representation of Infinite-Infinite Kripke Interpretations

Consider the following NTF example that requires an Infinite-Infinite model ...
```%------------------------------------------------------------------------------
tff(simple_spec,logic,
\$alethic_modal == [
\$constants == \$rigid,
\$quantification == \$constant,
\$modalities == \$modal_system_S5 ] ).

tff(person_type,type, person: \$tType).
tff(geoff_decl,type,geoff: person).
tff(alive_decl,type,alive: (person * \$int) > \$o).
tff(age_decl,type,age: (person * \$int) > \$int).

tff(before_geoff_born,axiom,
! [Year: \$int] :
( \$less(Year,1961)
=> ~ alive(geoff,Year) ) ).

tff(geoff_born,axiom,
alive(geoff,1961) ).

tff(geoff_alive_now,axiom,
alive(geoff,2022) ).

tff(geoff_age,axiom,
! [Year: \$int] :
( ( alive(geoff,Year)
=> age(geoff,Year) = \$difference(Year,1961) )
& ( ~ alive(geoff,Year)
=> age(geoff,Year) = -1 ) ) ).

tff(necessarily_alive_between,axiom,
! [StartYear: \$int,EndYear: \$int] :
( ( \$less(StartYear,EndYear)
& alive(geoff,StartYear)
& alive(geoff,EndYear) )
=> {\$necessary} @
( ! [BetweenYear: \$int] :
( ( \$greatereq(BetweenYear,StartYear)
& \$lesseq(BetweenYear,EndYear) )
=> alive(geoff,BetweenYear) ) ) ) ).

! [DeathYear: \$int] :
( ( alive(geoff,DeathYear)
& ~ alive(geoff,\$sum(DeathYear,1)) )
=> {\$necessary} @
( ! [Year: \$int] :
( \$greatereq(Year,DeathYear)
=> ~ alive(geoff,Year) ) ) ) ).

tff(might_live_another_year,axiom,
! [Year: \$int] :
( alive(geoff,Year)
=> {\$possible} @ ( alive(geoff,\$sum(Year,1)) ) ) ).

%----Adding this should make the axioms contradictory
% tff(must_die,axiom,
%     {\$necessary} @
%       ( ? [Year: \$int] :
%           ( \$greater(Year,1961)
%           & ~ alive(geoff,Year ) ) ).

%----This should be provable
% tff(might_live_long,conjecture,
%     {\$possible} @
%       ( ? [Year: \$int] :
%           ( age(geoff,Year) = 120
%           & alive(geoff,Year) ) ) ).

%------------------------------------------------------------------------------

```
Here will be a Infinite-Infinite model, when I find one ...
```[an error occurred while processing this directive]
```

## Visualization of Interpretations

Visualizing a finite interpretation:
• List of function and predicate symbols.
• When you click on a symbol you get a tree with branching factor equal to the number of domain elements, so that each branch corresponds to a domain element. The tree depth is the arity of the symbol, so that one branch represents one tuple of possible domain element arguments to the symbol.
• Each leaf is the domain element that the symbol is interpreted as for that branch's sequence of domain elements.
• Below the tree have a list of the domain elements.
• When you click on a domain element in the list lines are drawn from the domain element to the tree leaves with that value.
Here's a TFF interpretation encoded as a derivation that can be
viewed in IDV:
```%------------------------------------------------------------------------------
thf(a,negated_conjecture,
introduced(language,[level(0)]) ).

thf(f,negated_conjecture,
introduced(language,[level(0)]) ).

thf(john,negated_conjecture,
john: human,
introduced(language,[level(0)]) ).

introduced(language,[level(0)]) ).

thf(created_equal,negated_conjecture,
created_equal: (human * human) > \$o,
introduced(language,[level(0)]) ).

"john": human,

"gotA": human,

tcf(created_equal_john,plain,
"john": human,
inference(interpretation,[level(1)],[created_equal]) ).

tcf(created_equal_gotA,plain,
"gotA": human,
inference(interpretation,[level(1)],[created_equal]) ).

tcf(created_equal_john_john,plain,
"john": human,
inference(interpretation,[level(2)],[created_equal_john]) ).

tcf(created_equal_john_gotA,plain,
"gotA": human,
inference(interpretation,[level(2)],[created_equal_john]) ).

tcf(created_equal_gotA_john,plain,
"john": human,
inference(interpretation,[level(2)],[created_equal_gotA]) ).

tcf(created_equal_gotA_gotA,plain,
"gotA": human,
inference(interpretation,[level(2)],[created_equal_gotA]) ).

tcf(d_a,conjecture,

tcf(d_f,conjecture,

tcf(d_john,conjecture,
"john": human,
inference(interpretation,[level(3)],[john]) ).

tcf(d_gotA,conjecture,
"gotA": human,
inference(interpretation,[level(3)],[]) ).

cnf(d_true,conjecture,
\$true,
inference(interpretation,[level(3)],[created_equal_john_john,created_equal_gotA_gotA]) ).

%----Note this is not the true example, made some things false for illustration
cnf(d_false,conjecture,
\$false,
inference(interpretation,[level(3)],[created_equal_john_gotA,created_equal_gotA_john]) ).

fof(o_type,axiom,
\$o,
inference(type,[level(4)],[d_true,d_false]) ).

fof(human_type,axiom,
human,
inference(type,[level(4)],[d_john,d_gotA]) ).

inference(type,[level(4)],[d_a,d_f]) ).

%------------------------------------------------------------------------------

```
Visualizing an Kripke interpretation reachability relation: Draw the graph, e.g., using Graphviz.

## Verification of Models

Let ...
• Σ be an untyped first-order logic language, consisting of ...
• VΣ, a set of variables
• FΣ, a set of functions with arity
• PΣ, a set of predicate with arity
• φ be a formula written in Σ
• Ι be an interpretation of Σ, consisting of ...
• DΙ, a set of domain elements.
• FΙ, a mapping from elements of F applied to arguments from D, to D.
• RΙ, a mapping from elements of D applied to arguments from D, to {TRUE,FALSE}.
Ι can be a partial interpretation of Σ, but must be enough to interpret φ.
For example ...
• Σ ...
• VΣ = {Words starting uppercase}
• FΣ = {geoff/0, brotherOf/2}
• PΣ = {taller/2}
• Ι ...
• DΙ = {😀, 🕺}
• FΙ = { geoff → 😀, brotherOf(😀) → 🕺, brotherOf(🕺)😀}
• RΙ = { taller(😀,😀)FALSE, taller(😀,🕺)FALSE, taller(🕺,😀)TRUE, taller(🕺,🕺)FALSE}
• φ ...
• taller(brotherOf(geoff),geoff)
In the TPTP World the interpretation Ι is represented by formulae φΙ ...
• The domain is represented by an annotated formula with role domain, and a formula that uses equalities to list the formulae. To ensure that the domain elements written in a domain are understood to be distinct, "distinct object"s or numbers can be used. Otherwise their inequality must also be specified.
• The function map is represented by formulae with the role functors, and formulae that use equalities to express the mapping of functions applied to domain elements, to domain element values.
• The predicate map is represented by formulae with the role predicates, and formulae that use equalities to express the mapping of functions applied to domain elements, to truth values.
Currently the TPTP World specifies the roles fi_domain, fi_functors, and fi_predicates. The plan is to drop the fi_ prefixes, and allow infinite models.

• Let EφΙ be the set {e that are "domain element"s in φΙ}.
• Let inIφΙ(e) be the dΙDΙ corresponding to e ∈ EφΙ.

For example ...

• ```tff(myI_domain,domain,
! [X: \$i] : ( X = "face" | X = "stickman" ) ).```
• ```tff(myI_functions,functors,
( geoff = "face"
& brotherOf("face") = "stickman"
& brotherOf("stickman") = "face" ) ).```
• ```tff(myI_predicates,predicates,
( ~ taller("face","face")
& ~ taller("face","stickman")
& taller("stickman","face")
& ~ taller("stickman","stickman") ) ).
```

• EφΙ = {"face", "stickman"}
• inIφΙ("face") = 😀, inIφΙ("stickman") = 🕺

Proof that

if φΙ ⊨ φ then Ι ⊨ φ

• Let Σ' be ...
• V'Σ' = VΣ
• F'Σ' = FΣ ∪ EφΙ
• P'Σ' = PΣ
• Let Ι' be an interpretation ...
• DΙ' = DΙ
• FΙ' = FΙ ∪ {einIΙ(e)} for e ∈ EφΙ
• PΙ' = PΙ

• If Ι' ⊨ φ then Ι ⊨ φ, because φ contains nothing from EφΙ and Ι' is the same as Ι wrt all other symbols.
• Ι' ⊨ φΙ, because ...
• Let φΙ' be the "formulae" that result from applying Ι' to the e ∈ EφΙ in φΙ.
• Ι' ⊨ φΙ' iff Ι ⊨ φΙ'.
• Ι ⊨ φΙ' by the construction of Ι
• Ι' ⊨ φΙ'
• By undoing the application of Ι' to the e ∈ EφΙ in φΙ, Ι' ⊨ φΙ
• If φΙ ⊨ φ then Ι' ⊨ φ (every model of φΙ is a model of φ, Ι' is a model of φΙ, so Ι' is a model of φ)
• If φΙ ⊨ φ then Ι ⊨ φ
For example ...
• Σ' ...
• V'Σ' = {Words starting uppercase}
• F'Σ'' = {geoff/0, brotherOf/2, "face"/0, "stickman"/0}
• P'Σ' = {taller/2}
• Ι' ...
• DΙ' = {😀, 🕺}
• FΙ' = { geoff → 😀, "face" → 😀, "stickman" → 🕺,
brotherOf(😀) → 🕺, brotherOf(🕺)😀}
• RΙ' = { taller(😀,😀)FALSE, taller(😀,🕺)FALSE, taller(🕺,😀)TRUE, taller(🕺,🕺)FALSE}

• Ι' ⊨ taller(brotherOf(geoff),geoff), so
Ι ⊨ taller(brotherOf(geoff),geoff)
• Ι' ⊨ tff(myI_domain, ...
• If tff(myI_domain, ... taller(brotherOf(geoff),geoff) then
Ι' ⊨ taller(brotherOf(geoff),geoff)
• If tff(myI_domain, ... taller(brotherOf(geoff),geoff) then
Ι ⊨ taller(brotherOf(geoff),geoff)