Kripke Interpretations in One TX0 Formula

%------------------------------------------------------------------------------
tff(semantics,logic,
    $alethic_modal ==
      [ $domains == $constant,
        $designation == $rigid,
        $terms == $local,
        $modalities == $modal_system_M ] ).

tff(person_decl,type,person: $tType).
tff(product_decl,type,product: $tType).
tff(alex_decl,type,alex: person).
tff(chris_decl,type,chris: person).
tff(leo_decl,type,leo: product).
tff(work_hard_decl,type,work_hard: (person * product) > $o).
tff(gets_rich_decl,type,gets_rich: person > $o).

%----If there is a product that a person works hard on, then 
%----it's possible that the person will get rich.
tff(work_hard_to_get_rich,axiom,
    ! [P: person] :
      ( ? [R: product] : work_hard(P,R)
     => ( {$possible} @ (gets_rich(P)) ) ) ).

%----Nobody necessarily gets rich.
tff(not_all_get_rich,axiom,
    ~ ? [P: person] : ({$necessary} @ (gets_rich(P)) ) ).

%----Alex and Chris work hard on Leo-III.
tff(alex_works_on_leo,axiom,
    work_hard(alex,leo) ).

tff(chris_works_on_leo,axiom,
    work_hard(chris,leo) ).

%----Chris is not Alex
tff(chris_not_alex,axiom,
    chris != alex ).

%----It's possible that Alex gets rich but Chris does not.
tff(only_alex_gets_rich,conjecture,
    ( {$possible} @ (gets_rich(alex) & ~ gets_rich(chris)) ) ).
%------------------------------------------------------------------------------

%------------------------------------------------------------------------------
tff(semantics,logic,
    $alethic_modal ==
      [ $domains == $constant,
        $designation == $rigid,
        $terms == $local,
        $modalities == $modal_system_M ] ).

%----Declarations to fool Vampire when processing this file directly
% tff('$world_type',type,$world: $tType).
% tff('$local_world_decl',type,$local_world: $world).
% tff('$accessible_world_decl',type,$accessible_world: ($world * $world) > $o).
% tff('$in_world_decl',type,$in_world: ($world * $o) > $o).

tff(person_decl,type,    person: $tType).
tff(product_decl,type,   product: $tType).
tff(alex_decl,type,      alex: person).
tff(chris_decl,type,     chris: person).
tff(leo_decl,type,       leo: product).
tff(work_hard_decl,type, work_hard: (person * product) > $o).
tff(gets_rich_decl,type, gets_rich: person > $o).

tff(d_alex_decl,type,    d_alex: person).
tff(d_chris_decl,type,   d_chris: person).
tff(d_leo_decl,type,     d_leo: product).

tff(w1_decl,type,w1:     $world).
tff(w2_decl,type,w2:     $world).

tff(leo_workers,interpretation,
    ( ( ! [W: $world] : ( W = w1 | W = w2 )
      & $distinct(w1,w2)
      & $local_world = w2
      & $accessible_world(w1,w1)     %----Logic is M
      & $accessible_world(w2,w2)
      & $accessible_world(w1,w2) 
      & $accessible_world(w2,w1) )
    & $in_world(w1,
        ( ( ! [DP: person] : ( DP = d_alex | DP = d_chris )
          & $distinct(d_alex,d_chris)
          & ? [DP: person] : DP = d_alex
          & ? [DP: person] : DP = d_chris
          & ! [DP: product] : DP = d_leo
          & ? [DP: product] : DP = d_leo )
        & ( alex = d_alex
          & chris = d_chris
          & leo = d_leo )
        & ( work_hard(d_alex,d_leo)
          & work_hard(d_chris,d_leo)
          & gets_rich(d_alex)
          & gets_rich(d_chris) ) ) )
    & $in_world(w2,
        ( ( ! [DP: person] : ( DP = d_alex | DP = d_chris )
          & $distinct(d_alex,d_chris)
          & ? [DP: person] : DP = d_alex
          & ? [DP: person] : DP = d_chris
          & ! [DP: product] : DP = d_leo
          & ? [DP: product] : DP = d_leo )
        & ( alex = d_alex
          & chris = d_chris
          & leo = d_leo )
        & ( work_hard(d_alex,d_leo)
          & work_hard(d_chris,d_leo)
          & gets_rich(d_alex)
          & gets_rich(d_chris) ) ) ) ) ).
%------------------------------------------------------------------------------

%------------------------------------------------------------------------------
tff(semantics,logic,
    $alethic_modal == 
      [ $domains == $constant,
        $designation == $rigid,
        $terms == $local,
        $modalities == $modal_system_M ] ).

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

%------------------------------------------------------------------------------
tff(semantics,logic,
    $alethic_modal ==
      [ $domains == $constant,
        $designation == $rigid,
        $terms == $local,
        $modalities == $modal_system_M ] ).

%----Declarations to fool Vampire when processing this file directly
% tff('$world_type',type,$world: $tType).
% tff('$local_world_decl',type,$local_world: $world).
% tff('$accessible_world_decl',type,$accessible_world: ($world * $world) > $o).
% tff('$in_world_decl',type,$in_world: ($world * $o) > $o).

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(d_apple_decl,type,d_apple: fruit).
tff(d_banana_decl,type,d_banana: fruit).

tff(w1_decl,type,w1: $world).
tff(w2_decl,type,w2: $world).

tff(fruity_worlds,interpretation,
    ( ( ! [W: $world] : ( W = w1 | W = w2 )
      & $local_world = w1
      & $accessible_world(w1,w1)     %----Logic is M
      & $accessible_world(w2,w2)
      & $accessible_world(w1,w2) )
    & $in_world(w1,
        ( ( ! [DF: fruit] : ( DF = d_apple | DF = d_banana )
          & $distinct(d_apple,d_banana)
          & ? [DP: fruit] : ( DP = d_apple )
          & ? [DP: fruit] : ( DP = d_banana ) )
        & ( apple = d_apple
          & banana = d_banana )
        & ( healthy(d_apple)
          & healthy(d_banana)
          & ~ rotten(d_apple)
          & rotten(d_banana) ) ) )
    & $in_world(w2,
        ( ( ! [DF: fruit] : ( DF = d_apple | DF = d_banana )
          & $distinct(d_apple,d_banana)
          & ? [DP: fruit] : ( DP = d_apple )
          & ? [DP: fruit] : ( DP = d_banana ) )
        & ( apple = d_apple
          & banana = d_banana )
        & ( healthy(d_apple)
          & healthy(d_banana)
          & ~ rotten(d_apple)
          & ~ rotten(d_banana) ) ) ) ) ).
%------------------------------------------------------------------------------

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

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

%----Declarations to fool Vampire when processing this file directly
% tff('$world_type',type,$world: $tType).
% tff('$local_world_decl',type,$local_world: $world).
% tff('$accessible_world_decl',type,$accessible_world: ($world * $world) > $o).
% tff('$in_world_decl',type,$in_world: ($world * $o) > $o).

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(int2sequence_decl,type,int2sequence: $int > sequence).

tff(w1_decl,type,w1: $world).
tff(w2_decl,type,w2: $world).

tff(tossed_worlds,interpretation,
    ( ( ! [W: $world] : ( ( W = w1 ) | ( W = w2 ) )
      & $local_world = w1
      & $accessible_world(w1,w1)
      & $accessible_world(w2,w2)
      & $accessible_world(w1,w2) )
    & $in_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_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))) ) ) ) ) ) ) ).

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

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

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

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

%----Declarations to fool Vampire when processing this file directly
% tff('$world_type',type,$world: $tType).
% tff('$local_world_decl',type,$local_world: $world).
% tff('$accessible_world_decl',type,$accessible_world: ($world * $world) > $o).
% tff('$in_world_decl',type,$in_world: ($world * $o) > $o).

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(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(int2world_decl,type,int2world: $int > $world ).

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

%----Worlds before 1961 all think geoff was born that year
    & ! [IW: $int] :
        ( $less(IW,1961)
       => $in_world(int2world(IW),
%----Only one domain element for person
            ( ! [P: person] : ? [DP: d_person] : P = d2person(DP)
            & ! [DP: d_person] : DP = d_geoff
            & ? [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_world(int2world(IW),
            ( ! [P: person] : ? [DP: d_person] : P = d2person(DP)
            & ! [DP: d_person] : DP = d_geoff
            & ? [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) ) ) ) ) ) ) ) ).

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

%------------------------------------------------------------------------------
tff(simple_spec,logic,
    $alethic_modal == [
      $constants == $flexible,
      $quantification == $varying,
      $modalities == $modal_system_M ] ).

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

%------------------------------------------------------------------------------
tff(simple_spec,logic,
    $alethic_modal == [
      $constants == $flexible,
      $quantification == $varying,
      $modalities == $modal_system_M ] ).

%----Declarations to fool Vampire when processing this file directly
% tff('$world_type',type,$world: $tType).
% tff('$local_world_decl',type,$local_world: $world).
% tff('$accessible_world_decl',type,$accessible_world: ($world * $world) > $o).
% tff('$in_world_decl',type,$in_world: ($world * $o) > $o).

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(int2person_decl,type, int2person: $int > person ).

tff(int2world_decl,type,int2world: $int > $world ).

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

%----Now interpret each world
%----In world 0 
    & $in_world(int2world(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_world(int2world(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 ) ) ) ) ) ) ).
%------------------------------------------------------------------------------