Kripke Interpretations in One TX0 File

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

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_person_type,type,  d_person: $tType).
tff(d2person_decl,type,  d2person: d_person > person ).
tff(d_alex_decl,type,    d_alex: d_person).
tff(d_chris_decl,type,   d_chris: d_person).
tff(d_product_type,type, d_product: $tType).
tff(d2product_decl,type, d2product: d_product > product ).
tff(d_leo_decl,type,     d_leo: d_product).

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

tff(leo_workers_worlds,interpretation-world,
    ( ! [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) ) ). 

tff(leo_workers_w1_domain,
    interpretation-in_world(w1,interpretation-domain),
    $in_world(w1,
      ( ( ! [P: person] : ? [DP: d_person] : P = d2person(DP)
        & ! [DP: d_person] : ( DP = d_alex | DP = d_chris )
        & $distinct(d_alex,d_chris)
        & ? [DP: d_person] : ( DP = d_alex )
        & ? [DP: d_person] : ( DP = d_chris )
        & ! [DP1: d_person,DP2: d_person] : 
            ( d2person(DP1) = d2person(DP2) => DP1 = DP2 ) )
      & ( ! [P: product] : ? [DP: d_product] : P = d2product(DP)
        & ! [DP: d_product] : DP = d_leo
        & ? [DP: d_product] : DP = d_leo
        & ! [DP1: d_product,DP2: d_product] :
            ( d2product(DP1) = d2product(DP2) => DP1 = DP2 ) ) ) ) ).

tff(leo_workers_w2_domain,
    interpretation-in_world(w2,interpretation-domain),
    $in_world(w2,
      ( ( ! [P: person] : ? [DP: d_person] : P = d2person(DP)
        & ! [DP: d_person] : ( DP = d_alex | DP = d_chris )
        & $distinct(d_alex,d_chris)
        & ? [DP: d_person] : ( DP = d_alex )
        & ? [DP: d_person] : ( DP = d_chris )
        & ! [DP1: d_person,DP2: d_person] : 
            ( d2person(DP1) = d2person(DP2) => DP1 = DP2 ) )
      & ( ! [P: product] : ? [DP: d_product] : P = d2product(DP)
        & ! [DP: d_product] : DP = d_leo
        & ? [DP: d_product] : DP = d_leo
        & ! [DP1: d_product,DP2: d_product] :
            ( d2product(DP1) = d2product(DP2) => DP1 = DP2 ) ) ) ) ).

tff(leo_workers_w1_mappings,
    interpretation-in_world(w1,interpretation-mapping),
    $in_world(w1,
      ( ( alex = d2person(d_alex)
        & chris = d2person(d_chris)
        & leo = d2product(d_leo) )
      & ( work_hard(d2person(d_alex),d2product(d_leo))
        & work_hard(d2person(d_chris),d2product(d_leo))
        & gets_rich(d2person(d_alex))
        & gets_rich(d2person(d_chris)) ) ) ) ). 

tff(leo_workers_w2_mappings,
    interpretation-in_world(w2,interpretation-mapping),
    $in_world(w2,
      ( ( alex = d2person(d_alex)
        & chris = d2person(d_chris)
        & leo = d2product(d_leo) )
      & ( work_hard(d2person(d_alex),d2product(d_leo))
        & work_hard(d2person(d_chris),d2product(d_leo))
        & ~ gets_rich(d2person(d_alex))
        & ~ gets_rich(d2person(d_chris)) ) ) ) ). 
%------------------------------------------------------------------------------

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

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_person_type,type,  d_person: $tType).
tff(d2person_decl,type,  d2person: d_person > person ).
tff(d_alex_decl,type,    d_alex: d_person).
tff(d_chris_decl,type,   d_chris: d_person).
tff(d_product_type,type, d_product: $tType).
tff(d2product_decl,type, d2product: d_product > product ).
tff(d_leo_decl,type,     d_leo: d_product).

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

tff(leo_workers_worlds,interpretation-world,
    ( ! [W: $world] : ( W = w1 | W = w2 )
    & $distinct(w1,w2)
    & $local_world = w2
    & $accessible_world(w1,w1) & $accessible_world(w2,w2)
    & $accessible_world(w1,w2) & $accessible_world(w2,w1) ) ). 

tff(leo_workers_w1_person,
    interpretation-in_world(w1,interpretation-domain(person,d_person)),
    $in_world(w1,
      ( ! [P: person] : ? [DP: d_person] : P = d2person(DP)
      & ! [DP: d_person] : ( DP = d_alex | DP = d_chris )
      & $distinct(d_alex,d_chris)
      & ? [DP: d_person] : ( DP = d_alex )
      & ? [DP: d_person] : ( DP = d_chris )
      & ! [DP1: d_person,DP2: d_person] : 
          ( d2person(DP1) = d2person(DP2) => DP1 = DP2 ) ) ) ).

tff(leo_workers_w1_product,
    interpretation-in_world(w1,interpretation-domain(product,d_product)),
    $in_world(w1,
      ( ! [P: product] : ? [DP: d_product] : P = d2product(DP)
      & ! [DP: d_product] : DP = d_leo
      & ? [DP: d_product] : DP = d_leo
      & ! [DP1: d_product,DP2: d_product] :
          ( d2product(DP1) = d2product(DP2) => DP1 = DP2 ) ) ) ).

tff(leo_workers_w2_person,
    interpretation-in_world(w2,interpretation-domain(person,d_person)),
    $in_world(w2,
      ( ! [P: person] : ? [DP: d_person] : P = d2person(DP)
      & ! [DP: d_person] : ( DP = d_alex | DP = d_chris )
      & $distinct(d_alex,d_chris)
      & ? [DP: d_person] : ( DP = d_alex )
      & ? [DP: d_person] : ( DP = d_chris )
      & ! [DP1: d_person,DP2: d_person] : 
          ( d2person(DP1) = d2person(DP2) => DP1 = DP2 ) ) ) ).

tff(leo_workers_w2_product,
    interpretation-in_world(w2,interpretation-domain(product,d_product)),
    $in_world(w2,
      ( ! [P: product] : ? [DP: d_product] : P = d2product(DP)
      & ! [DP: d_product] : DP = d_leo
      & ? [DP: d_product] : DP = d_leo
      & ! [DP1: d_product,DP2: d_product] :
          ( d2product(DP1) = d2product(DP2) => DP1 = DP2 ) ) ) ).

tff(leo_workers_w1_alex,
    interpretation-in_world(w1,interpretation-mapping(alex,d_person)),
    $in_world(w1, ( alex = d2person(d_alex) )) ).

tff(leo_workers_w2_alex,
    interpretation-in_world(w2,interpretation-mapping(alex,d_person)),
    $in_world(w2, ( alex = d2person(d_alex) )) ).

tff(leo_workers_w1_chris,
    interpretation-in_world(w1,interpretation-mapping(chris,d_person)),
    $in_world(w1, ( chris = d2person(d_chris) )) ).

tff(leo_workers_w2_chris,
    interpretation-in_world(w2,interpretation-mapping(chris,d_person)),
    $in_world(w2, ( chris = d2person(d_chris) )) ).

tff(leo_workers_w1_leo,
    interpretation-in_world(w1,interpretation-mapping(leo,d_product)),
    $in_world(w1, ( leo = d2product(d_leo) )) ).

tff(leo_workers_w2_leo,
    interpretation-in_world(w2,interpretation-mapping(leo,d_product)),
    $in_world(w2, ( leo = d2product(d_leo) )) ).

tff(leo_workers_w1_work_hard,
    interpretation-in_world(w1,interpretation-mapping(work_hard,$o)),
    $in_world(w1,
      ( work_hard(d2person(d_alex),d2product(d_leo))
      & work_hard(d2person(d_chris),d2product(d_leo)) )) ).

tff(leo_workers_w2_work_hard,
    interpretation-in_world(w2,interpretation-mapping(work_hard,$o)),
    $in_world(w2,
      ( work_hard(d2person(d_alex),d2product(d_leo))
      & work_hard(d2person(d_chris),d2product(d_leo)) )) ).

tff(leo_workers_w1_gets_rich,
    interpretation-in_world(w1,interpretation-mapping(gets_rich,$o)),
    $in_world(w1,
      ( gets_rich(d2person(d_alex)) & gets_rich(d2person(d_chris)) ) ) ). 

tff(leo_workers_w2_gets_rich,
    interpretation-in_world(w2,interpretation-mapping(gets_rich,$o)),
    $in_world(w2,
      ( ~ gets_rich(d2person(d_alex)) & ~ gets_rich(d2person(d_chris)) ) ) ). 
%------------------------------------------------------------------------------

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

[an error occurred while processing this directive]