Interpretation Representation and Model Verification

by Geoff Sutcliffe, Alex Steen, Pascal Fontaine, Jack McKeown


Motivation

Why is Model Finding Useful?

Is there a need for model finding systems that:
  1. Give only a "yes", indicating that there is a model.
  2. Give only a "yes, finite", indicating that there is a finite model.
  3. Output a model in some form
  4. Output a finite model in some form

Representation of Interpretations

Infinite domains are necessary as soon as the formula language contains any numbers on an infinite domain (not arithemetic modulo). Infinite domains are also necessary for other (non-numeric) applications, e.g., those that involve modeling time. Types of interpretations include:

Properties of Different Representations


Representation of Interpretations in the TPTP World


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 ) ).

fof(distinct_grades,axiom,
    a != f ).

fof(grades_not_human,axiom,
    ! [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 countermodel 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(grade_type,type,         grade: $tType ).
tff(john_decl,type,          john: man ).
tff(a_decl,type,             a: grade ).
tff(f_decl,type,             f: grade ).
tff(grade_of_decl,type,      grade_of: man > 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 ).

tff(distinct_grades,axiom,
    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(grade_type,type,         grade: $tType ).
tff(john_decl,type,          john: man ).
tff(a_decl,type,             a: grade ).
tff(f_decl,type,             f: grade ).
tff(grade_of_decl,type,      grade_of: man > grade ).
tff(created_equal_decl,type, created_equal: ( man * man ) > $o ).

tff(d_man_type,type,         d_man: $tType).
tff(d_grade_type,type,       d_grade: $tType).
tff(d2man_decl,type,         d2man: d_man > man ).
tff(d2grade_decl,type,       d2grade: d_grade > grade ).

tff(d_john_decl,type,        d_john: d_man ).
tff(d_gotA_decl,type,       d_gotA: 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 domain for man is d_man
    ( ( ! [M: man] : ? [DM: d_man] : M = d2man(DM)
%----The d_man elements are d_john and d_gotA
      & ! [DM: d_man] : ( DM = d_john | DM = d_gotA )
      & $distinct(d_john,d_gotA)
%----The type promoter is a bijection
      & ! [DM1: d_man,DM2: d_man] : 
          ( d2man(DM1) = d2man(DM2) => DM1 = DM2 )
%----The domain for grade is d_grade
      & ! [G: grade] : ? [DG: d_grade] : G = d2grade(DG)
%----The two d_grade elements are d_a and d_f
      & ! [DG: d_grade]: ( DG = d_a | DG = d_f )
      & $distinct(d_a,d_f)
%----The type promoter is a bijection 
      & ! [DG1: d_grade,DG2: d_grade] : 
          ( d2grade(DG1) = d2grade(DG2) => DG1 = DG2 ) )
%----Interpret terms via the type-promoted domain 
    & ( a = d2grade(d_a)
      & f = d2grade(d_f)
      & john = d2man(d_john)
      & grade_of(d2man(d_john)) = d2grade(d_f)
      & grade_of(d2man(d_gotA)) = d2grade(d_a) )
%----Interpret atoms as true of false
    & ( created_equal(d2man(d_john),d2man(d_john))
      & created_equal(d2man(d_john),d2man(d_gotA))
      & created_equal(d2man(d_gotA),d2man(d_john))
      & created_equal(d2man(d_gotA),d2man(d_gotA)) ) ) ).
%----If John was not equal to the man who got an A:
%---- & ~ created_equal(d2man(d_john),d2man(d_gotA))
%---- & ~ created_equal(d2man(d_gotA),d2man(d_john))

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

Hmmm, should the types be inside the interpretation?

TFF_Finite.s.p is the proof problem to verify the countermodel using the technique discussed in Verification of Models.


Representation of TXF Interpretations


Representation of THF Interpretations


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 countably infinite domains (e.g., the integers), or even domains of larger cardinalities (e.g., the reals). Consider the following TFF example that requires an integer size domain ...
%------------------------------------------------------------------------------
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) ) ).

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

Here's a model using closed terms representing Peano numbers as 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(peano_type,type,          peano: $tType).
tff(zero_decl,type,           zero: peano ).
tff(s_decl,type,              s: peano > peano ).
tff(peano2person_decl,type,peano2person: peano > person ).
tff(peano_less_decl,type,     peano_less: ( peano * peano ) > $o ).

tff(people,interpretation,
%----Domain for type person is the Peano numbers
    ( ( ! [P: person] : ? [I: peano] : P = peano2person(I)
%----The type promoter is a bijection (injective and surjective)
      & ! [I1: peano,I2: peano] :
          ( peano2person(I1) = peano2person(I2) => I1 = I2 )
%----Relationships between Peano numbers
      & ! [I1: peano,I2: peano,I3: peano] :
          ( peano_less(I1,s(I1))
          & ( ( peano_less(I1,I2)
              & peano_less(I2,I3) )
           => peano_less(I1,I3) )
          & ( peano_less(I1,I2)
           => I1 != I2 ) ) )
%----Mapping people to integers. Note that Bob's ancestors will be interpreted
%----as negative integers.
    & ( bob = peano2person(zero)
      & ! [I: peano] :
          child_of(peano2person(I)) = peano2person(s(I)) )
%----Interpretation of descendancy
    & ( ! [A: peano,D: peano] :
          ( is_descendant(peano2person(A),peano2person(D))
        <=> peano_less(A,D) ) ) ) ).

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

TFF_Peano.s.p is the proof problem to verify the model using the technique discussed in Verification of Models. It can be solved by Vampire.

Here's a model using the 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(int2person_decl,type,    int2person: $int > person ).

tff(people,interpretation,
%----Domain for type person is the integers
    ( ( ! [P: person] : ? [I: $int] : int2person(I) = P
%----The type promoter is a bijection (injective and surjective)
      & ! [I1: $int,I2: $int] : 
          ( int2person(I1) = int2person(I2) => I1 = I2 ) )
%----Mapping people to integers. Note that Bob's ancestors will be interpreted 
%----as negative integers.
    & ( bob = int2person(0)
      & ! [I: $int] : child_of(int2person(I)) = int2person($sum(I,1)) )
%----Interpretation of descendancy
    & ! [A: $int,D: $int] : 
        ( is_descendant(int2person(A),int2person(D)) <=> $less(A,D) ) ) ).

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

TFF_Integer.s.p is the proof problem to verify the model using the technique discussed in Verification of Models. It can be solved by Vampire.

Finite and infinite domains can be mixed. Here's a problem that can be proven by Vampire. With the conjecture modified as below, it has a countermodel with integer domains for the X and Y positions (mimicing the logic), and a finite domain for the Z level.

tff(level_type,type,level: $tType).
tff(ground_decl,type,ground: level).
tff(middle_decl,type,middle: level).
tff(top_decl,type,top: level).
tff(space_decl,type,space: level).

tff(possible_position_decl,type,
    possible_position: ($int * $int * level) > $o ).

tff(only_four_distinct_levels,axiom,
    ( ! [Z: level] :
        ( Z = ground
        | Z = middle
        | Z = top 
        | Z = space ) 
    & ( ground != middle
      & ground != top
      & ground != space
      & middle != top
      & middle != space
      & top != space ) ) ).
%    & $distinct(ground,middle,top,space) ) ).

tff(start_at_origin,axiom,
    possible_position(0,0,ground) ).

tff(move_X,axiom,
    ! [X: $int,Y: $int,Z: level] :
      ( possible_position(X,Y,Z)
     => ( possible_position($difference(X,1),Y,Z)
        & possible_position($sum(X,1),Y,Z) ) ) ).

tff(move_Y,axiom,
    ! [X: $int,Y: $int,Z: level] :
      ( possible_position(X,Y,Z)
     => ( possible_position(X,$difference(Y,1),Z)
        & possible_position(X,$sum(Y,1),Z) ) ) ).

tff(move_Z,axiom,
    ! [X: $int,Y: $int] :
      ( ( possible_position(X,Y,ground)
       => possible_position(X,Y,middle) )
      & ( possible_position(X,Y,middle)
       => ( possible_position(X,Y,ground)
          & possible_position(X,Y,top) ) )
      & ( possible_position(X,Y,top)
       => possible_position(X,Y,middle) ) ) ).

tff(can_fly,conjecture,
    possible_position(3,-5,space) ).

Here's the countermodel ...
tff(level_type,type,level: $tType).
tff(ground_level_decl,type,ground: level).
tff(middle_level_decl,type,middle: level).
tff(top_level_decl,type,top: level).
tff(space_level_decl,type,space: level).
tff(possible_position_decl,type,
    possible_position: ($int * $int * level) > $o ).

tff(d_level_type,type,d_level: $tType).
tff(d_ground_decl,type,d_ground: d_level).
tff(d_middle_decl,type,d_middle: d_level).
tff(d_top_decl,type,d_top: d_level).
tff(d_space_decl,type,d_space: d_level).
tff(d2level_decl,type,d2level: d_level > level).

tff(drone,interpretation,
    ( ( ! [L: level] : ? [DL: d_level] : L = d2level(DL)
      & ! [Z: d_level] : ( Z = d_ground | Z = d_middle | Z = d_top | Z = d_space )
      & ( d_ground != d_middle
        & d_ground != d_top
        & d_ground != d_space
        & d_middle != d_top
        & d_middle != d_space
        & d_top != d_space )
%     & $distinct(ground,middle,top,space)
%----The type promoter is a bijection (injective and surjective)
      & ! [DL1: d_level,DL2: d_level] : ( d2level(DL1) = d2level(DL2) => DL1 = DL2 ) )
    & ! [X: $int,Y: $int] :
        ( possible_position(X,Y,d2level(d_ground))
        & possible_position(X,Y,d2level(d_middle))
        & possible_position(X,Y,d2level(d_top))
        & ~ possible_position(X,Y,d2level(d_space)) ) ) ).


TFF_Peano.s.p is the proof problem to verify the model using the technique discussed in Verification of Models. It can be solved by Vampire.


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 $local_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 can be proven by Leo-III. With the conjecture modified as below, it has a countermodel with a finite number of worlds each of which has a finite domain (hence a "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(apple_not_banana,axiom,
    apple != banana ).

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

tff(fruit_possibly_not_rotten,axiom,
    ! [F: fruit] : {$possible} @ (~ rotten(F)) ).

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

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

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

After using NTF2THF to embed the problem into TH0, Nitpick finds a countermodel that I converted by hand into TPTP format ...
%------------------------------------------------------------------------------
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(d2fruit_decl,type, d2fruit: 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 )
      & $local_ki_world = w1
      & $accessible_ki_world(w1,w1)     %----Logic is T
      & $accessible_ki_world(w2,w2)
      & $accessible_ki_world(w1,w2) )
    & ( $in_ki_world(w1)
     => ( ( ! [F: fruit] : ? [DF: d_fruit] : F = d2fruit(DF)
          & ! [DF: d_fruit] : ( DF = d_apple | DF = d_banana )
          & $distinct(d_apple,d_banana)
          & ! [DF1: d_fruit,DF2: d_fruit] : 
              ( d2fruit(DF1) = d2fruit(DF2) => DF1 = DF2 ) )
        & ( apple = d2fruit(d_apple)
          & banana = d2fruit(d_banana) )
        & ( healthy(d2fruit(d_apple))
          & healthy(d2fruit(d_banana))
          & ~ rotten(d2fruit(d_apple))
          & rotten(d2fruit(d_banana)) ) ) )
    & ( $in_ki_world(w2)
     => ( ( ! [F: fruit] : ? [DF: d_fruit] : F = d2fruit(DF)
          & ! [DF: d_fruit] : ( DF = d_apple | DF = d_banana )
          & $distinct(d_apple,d_banana)
          & ! [DF1: d_fruit,DF2: d_fruit] : 
              ( d2fruit(DF1) = d2fruit(DF2) => DF1 = DF2 ) )
        & ( apple = d2fruit(d_apple)
          & banana = d2fruit(d_banana) )
        & ( healthy(d2fruit(d_apple))
          & healthy(d2fruit(d_banana))
          & ~ rotten(d2fruit(d_apple))
          & ~ rotten(d2fruit(d_banana)) ) ) )) ).

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

NTF_Finite-Finite.s.p is the proof problem to verify the countermodel using the technique discussed in Verification of Models. It can be solved by Vampire.


Representation of Finite-Infinite Kripke Interpretations

Here's a problem that can be proven by Leo-III. With the conjecture modified as below, it has a countermodel that requires (I think, at least it uses) only two worlds, and they have infinite domains because sequences of tosses are infinite and different sequences are unequal.
%------------------------------------------------------------------------------
tff(simple_spec,logic,
    $alethic_modal == [
      $constants == $rigid,
      $quantification == $constant,
      $modalities == $modal_system_S4 ] ).

tff(sequence_type,type, sequence: $tType ).
tff(null_decl,type, null: sequence ).
tff(toss_decl,type, toss: sequence > sequence ).
tff(all_heads_decl,type, all_heads: sequence > $o ).

tff(different_sequences,axiom,
    ! [S: sequence] : 
      ( ( toss(S) != null )
      & ( toss(S) != S ) ) ).

tff(injection,axiom,
    ! [S1: sequence,S2: sequence] :
      ( ( toss(S1) = toss(S2) )
     => ( S1 = S2 ) ) ).

tff(all_heads_possible,axiom,
    ! [S: sequence] :
      ( all_heads(S)
     => ( {$possible} @ 
          ( all_heads(toss(S)) ) ) ) ).

tff(no_heads,axiom,
    all_heads(null) ).
          
tff(two_heads_necessary,conjecture,
    {$necessary} @
      ( ? [S: sequence] : 
          ( all_heads(S) 
          & all_heads(toss(S)) ) ) ).

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

After using NTF2THF to embed the problem into TH0, Nitpick cannot find a countermodel ... as expected ... Nitpick can find only finite models. So I hand-rolled a countermodel. In the countermodel sequences of tosses are represented by integers, with the null sequence represented by 1. The encoding is easy to see in binary, reading the tosses left-to-right and the bits right-to-left. If the last bit is 0 a head was tossed, if 1 a tail was tossed: null = 1 = 0001, head = 2 = 0010, tail = 3 = 0011, head-head = 4 = 0100, head-tail = 5 = 0101, tail-head = 6 = 0110, tail-tail = 7 = 0111, head-head-head = 8 = 1000, head-head-tail = 9 = 1001, head-tail-head = 10 = 1010, head-tail-tail = 11 = 1011, tail-head-head = 12 = 1100, etc, etc. The local world tosses a sequence of heads, interpreted as integer domain elements that are powers of 2. The other world first tosses a tail, represented by 3, and then tosses all heads, interpreted as integer domain elements that are powers of 2 multiplied by 3. There is no definition of sequences interpreted as integer domain elements less or equal to 0, but they are not "all_heads".
%------------------------------------------------------------------------------
tff(sequence_type,type, sequence: $tType ).
tff(null_decl,type, null: sequence ).
tff(toss_decl,type, toss: sequence > sequence ).
tff(all_heads_decl,type, all_heads: sequence > $o ).

tff(w1_decl,type,w1: $ki_world).
tff(w2_decl,type,w2: $ki_world).
tff(int2sequence_decl,type,int2sequence: $int > sequence).

tff(tossed_worlds,interpretation,
    ( ( ! [W: $ki_world] : ( ( W = w1 ) | ( W = w2 ) )
      & $local_ki_world = w1
      & $accessible_ki_world(w1,w1)
      & $accessible_ki_world(w2,w2)
      & $accessible_ki_world(w1,w2) )
    & ( $in_ki_world(w1)
%----The domain for type sequence is the integers
     => ( ( ! [S: sequence] : ? [I: $int] : S = int2sequence(I)
%----The type promoter is a bijection
          & ! [X: $int,Y: $int] : 
              ( int2sequence(X) = int2sequence(Y) => X = Y ) )
        & ( null = int2sequence(1)
%----In world w1 the first toss is a head. This is redundant.
          & toss(int2sequence(1)) = int2sequence(2)
          & ! [I: $int] : 
              toss(int2sequence(I)) = int2sequence($product(I,2)) )
        & ( all_heads(int2sequence(1))
          & ! [I: $int] :
              ( all_heads(int2sequence(I))
            <=> ( $greatereq(I,2)
                & ( $remainder_e(I,2) = 0 )
                & all_heads(int2sequence($quotient_e(I,2))) ) ) ) ) )
    & ( $in_ki_world(w2)
     => ( ( ! [S: sequence] : ? [I: $int] : S = int2sequence(I)
          & ! [X: $int,Y: $int] : 
              ( int2sequence(X) = int2sequence(Y) => X = Y ) )
        & ( null = int2sequence(1)
%----In world w2 the first toss is a tail
          & toss(int2sequence(1)) = int2sequence(3)
          & ! [I: $int] : 
              ( I != 1
             => toss(int2sequence(I)) = int2sequence($product(I,2)) ) )
        & ( all_heads(int2sequence(1))
          & ! [I: $int] :
              ( all_heads(int2sequence(I))
            <=> ( $greatereq(I,2)
                & ( $remainder_e(I,2) = 0 )
                & all_heads(int2sequence($quotient_e(I,2))) ) ) ) ) ) ) ).

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

NTF_Finite-Infinite.s.p is the proof problem to verify the countermodel using the technique discussed in Verification of Models. It can be solved by Vampire.


Representation of Infinite-Finite Kripke Interpretations

This example requires (I think) an infinite number of worlds. The interpretation in the local world will have an infinite domain, but all the other worlds' domains need only a single element (one of the domain elements from the local world). All the domain elements of the local 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).

tff(like_exactly_one_person,axiom,
    ? [P: person] :
      ( like(P)
      & ! [OP: person] :
          ( like(OP)
         => OP = P ) ) ).

%----Infinite people here. 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_here,axiom-local,
    like(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(int2ki_world_decl,type,int2ki_world: $int > $ki_world ).
tff(int2person_decl,type, int2person: $int > person ).

tff(like_geoff,interpretation,
%----An infinite number of worlds, numbered by naturals
    ( ( ! [I: $int] : 
          ( $greatereq(I,0)
         => ? [W: $ki_world] : int2ki_world(I) = W )
      & $local_ki_world = int2ki_world(0)
%----The type promoter is a bijection (injective and surjective)
      & ! [I1: $int,I2: $int] : 
          ( ( int2ki_world(I1) = int2ki_world(I2) ) => ( I1 = I2 ) )
      & ! [W: $ki_world] : ? [I: $int] : int2ki_world(I) = W
%----World 0 can access itself (system T)
      & $accessible_ki_world(int2ki_world(0),int2ki_world(0))
%----World 0 can access all other worlds
      & ! [I: $int] : 
          ( $greater(I,0)
         => $accessible_ki_world(int2ki_world(0),int2ki_world(I)) ) )

%----Now interpret each world
%----In world 0 
    & ( $in_ki_world(int2ki_world(0))
%----The domain for type person is the integers
     => ( ( ! [P: person] : ? [I: $int] : P = int2person(I)
%----The type promoter is a bijection (injective and surjective)
          & ! [I1: $int,I2: $int] : 
              ( int2person(I1) = int2person(I2) => I1 = I2 ) )
%----geoff is interpreted as 0
        & ( geoff = int2person(0)
%----id_of coincides with the domain elements
          & ! [I: $int] : id_of(int2person(I)) = I )
%----like is true for 0 (and only 0 by next part for all worlds)
        & like(int2person(0) ) ) )
%----In all worlds
    & ! [IW: $int] :
        ( ( $greatereq(IW,0)
          & $in_ki_world(int2ki_world(IW)) )
%----The type promoter is a bijection (injective and surjective)
       => ( ( ! [P: person] : ? [I: $int] : P = int2person(I)
            & ! [I1: $int,I2: $int] : 
                ( int2person(I1) = int2person(I2) => I1 = I2 ) )
%----geoff is interpreted as the world number
          & ( geoff = int2person(IW)
%----id_of coincides with the world
            & id_of(int2person(IW)) = IW )
%----Like the person who is interpreted as this world number (geoff)
          & ( like(int2person(IW)) 
%----Like only this one person
            & ! [ID: $int] :
                ( like(int2person(ID))
              <=> ID = IW ) ) ) ) ) ).

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

NTF_Infinite-Finite.s.p is the proof problem to verify the countermodel using the technique discussed in Verification of Models. It can be solved by Vampire.


Representation of Infinite-Infinite Kripke Interpretations

Here's a problem that I think should be provable, but none of the ATP systems I know can (after conversion to THF, Leo-III does not have the arithmetic power, E, Vampire, and Zipperposition don't do arithmetic (at least in THF), cvc5 gives parse error). With the conjecture commented out as below, the axioms have a an Infinite-Infinite model (I think).
%------------------------------------------------------------------------------
tff(simple_spec,logic,
    $alethic_modal == [
      $constants == $rigid,
      $quantification == $constant,
      $modalities == $modal_system_T ] ).

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(born_by_1961,axiom,
    ? [BirthYear: $int] :
      ( $lesseq(BirthYear,1961)
      & ! [PreBirthYear: $int] :
          ( $less(PreBirthYear,BirthYear)
         => ( ~ alive(geoff,PreBirthYear)
            & age(geoff,PreBirthYear) = -1 ) )
      & ! [FromBirthYear: $int] :
          ( $greatereq(FromBirthYear,BirthYear)
         => ( alive(geoff,FromBirthYear)
            & age(geoff,FromBirthYear) = $difference(FromBirthYear,BirthYear)) ) ) ).

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) ) ) ) ).

tff(necessarily_dead_after,axiom,
    ! [DeathYear: $int] :
      ( ( alive(geoff,DeathYear)
        & ~ alive(geoff,$sum(DeathYear,1)) )
     => {$necessary} @
          ( ! [Year: $int] :
              ( $greater(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's a in which there are an infinite number of worlds - one for each integer numbered year, an infinite number of ages as integers, and just one person in each world.
%------------------------------------------------------------------------------
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(int2ki_world_decl,type,int2ki_world: $int > $ki_world ).

tff(d_person_type,type,d_person: $tType).
tff(d_geoff_decl,type,d_geoff: d_person).
tff(d2person_decl,type,d2person: d_person > person).

tff(long_live_geoff,interpretation,
%----An infinite number of worlds, numbered by naturals
    ( ( ! [I: $int] : 
        ? [W: $ki_world] : int2ki_world(I) = W
%----The type promoter is a bijection (injective and surjective)
      & ! [I1: $int,I2: $int] : 
          ( int2ki_world(I1) = int2ki_world(I2) => I1 = I2 )
      & ! [W: $ki_world] : ? [I: $int] : int2ki_world(I) = W
%----Worlds can access themselves and greater indexed worlds (worlds in the future)
      & ! [P: $int,F: $int] : 
          ( $greatereq(F,P)
         => $accessible_ki_world(int2ki_world(P),int2ki_world(F)) ) )

%----Worlds before 1961 all think geoff was born that year
    & ! [IW: $int] :
        ( ( $less(IW,1961)
          & '$in_ki_world'(int2ki_world(IW)) )
%----Only one domain element for person
       => ( ( ! [P: person] : ? [DP: d_person] : P = d2person(DP)
            & ! [DP: d_person] : DP = d_geoff
%----The type promoter is a bijection (injective and surjective)
            & ! [X: d_person,Y: d_person] :
                ( d2person(X) = d2person(Y) => X = Y ) )
          & geoff = d2person(d_geoff)
%----Alive and age interpretation
          & ! [Y: $int] :
              ( $less(Y,IW)
             => ( ~ alive(d2person(d_geoff),Y)
                & age(d2person(d_geoff),Y) = -1 ) )
          & alive(d2person(d_geoff),IW)
          & age(d2person(d_geoff),IW) = 0
          & ! [Y: $int] :
              ( $greater(Y,IW)
             => ( alive(d2person(d_geoff),Y)
                & age(d2person(d_geoff),Y) = $difference(Y,IW) ) ) ) ) )

%----Worlds from 1961 know geoff was born in 1961. geoff lives forever!
    & ! [IW: $int] :
        ( ( $greatereq(IW,1961)
          & '$in_ki_world'(int2ki_world(IW)) )
       => ( ( ! [P: person] : ? [DP: d_person] : P = d2person(DP)
            & ! [DP: d_person] : DP = d_geoff
            & ! [X: d_person,Y: d_person] :
                ( d2person(X) = d2person(Y) => X = Y ) )
          & geoff = d2person(d_geoff)
          & ! [Y: $int] :
              ( ( $less(Y,1961)
               => ( ~ alive(d2person(d_geoff),Y)
                  & age(d2person(d_geoff),Y) = -1 ) )
              & ( ( $greatereq(Y,1961)
                  & $less(Y,IW) )
               => ( alive(d2person(d_geoff),Y)
                  & age(d2person(d_geoff),Y) = $difference(Y,1961) ) ) )
          & alive(d2person(d_geoff),IW)
          & age(d2person(d_geoff),IW) = $difference(IW,1961)
          & ! [Y: $int] :
              ( $greater(Y,IW)
             => ( alive(d2person(d_geoff),Y)
                & age(d2person(d_geoff),Y) = $difference(Y,1961) ) ) ) ) ).

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

NTF_Infinite-Infinite.s.p is the proof problem to verify the countermodel using the technique discussed in Verification of Models.


Visualization of Interpretations

Visualizing a finite interpretation: Here's a TFF interpretation encoded as a derivation that can be
viewed in IDV:
%------------------------------------------------------------------------------
thf(a,negated_conjecture,
    a: grade,
    introduced(language,[level(0)]) ).

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

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

thf(grade_of,negated_conjecture,
    grade_of: human > grade,
    introduced(language,[level(0)]) ).

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

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

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

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,
    "a": grade,
    inference(interpretation,[level(3)],[a,grade_of_gotA]) ).

tcf(d_f,conjecture,
    "f": grade,
    inference(interpretation,[level(3)],[f,grade_of_john]) ).

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]) ).

fof(grade_type,axiom,
    grade,
    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 ... For example ... In the TPTP World the interpretation Ι is represented by formulae φΙ ... 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.

For example ...

Proof that

    if φΙ ⊨ φ then Ι ⊨ φ

For example ...