Kripke Interpretations

New defined symbols

In TX0

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

tff(child_type,type,    child: $tType ).
tff(adult_type,type,    adult: $tType ).
tff(agatha_decl,type,   agatha: adult ).
tff(charly_decl,type,   charly: child ).
tff(quiet_decl,type,    quiet: child > $o ).
tff(sleepy_decl,type,   sleepy: adult > $o ).
tff(peaceful_decl,type, peaceful: child > $o ).
tff(serves_decl,type,   serves: adult > child ).
tff(rains_decl,type,    rains: $o ).

tff(a1,axiom,
    ! [C: child] :
      ~ ( ~quiet(C) & ? [A: adult] : sleepy(A) ) ).

tff(a2,axiom,
    ( ( rains & ? [C: child] : quiet(C) )
   => ! [C: child] : ~peaceful(C) ) ).

tff(a3,axiom,
    ( peaceful(charly)
    | ( ~quiet(charly) & quiet(serves(agatha)) ) ) ).

tff(a4,axiom,
    ~quiet(charly) => ! [C: child] : ~quiet(C) ).

tff(a5,axiom,
    {$necessary} @ ( peaceful(charly) => rains ) ).

tff(c,conjecture,
    {$possible} @ (~ rains) ).
%------------------------------------------------------------------------------

Keep logic specification

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

Keep problem types

tff(child_type,type,    child: $tType ).
tff(adult_type,type,    adult: $tType ).
tff(agatha_decl,type,   agatha: adult ).
tff(charly_decl,type,   charly: child ).
tff(quiet_decl,type,    quiet: child > $o ).
tff(sleepy_decl,type,   sleepy: adult > $o ).
tff(peaceful_decl,type, peaceful: child > $o ).
tff(serves_decl,type,   serves: adult > child ).
tff(rains_decl,type,    rains: $o ).

Declare new domain types to declare domain elements

tff(child_d_decl,type,  child_d: $tType).
tff(adult_d_decl,type,  adult_d: $tType).
tff(child_1_decl,type,  child_1: child_d).
tff(adult_1_decl,type,  adult_1: adult_d).

... and add type promotion functions ...

tff(d2child_decl,type, d2child: child_d > child).
tff(d2adult_decl,type, d2adult: adult_d > adult).

Declare worlds

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

New role interpretation

tff(people_worlds,interpretation-subrole,

Specify worlds and accessibility


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

In each world

tff(people_domains,interpretation-domains,
    ( $in_world(w1,
    & $in_world(w2,
    & $in_world(w3,

Specify domains

tff(people_domains,interpretation-domains,
    ( $in_world(w1,
        ( ! [C: child] : ? [CD: child_d] : ( C = d2child(CD) )
        & ! [CD: child_d] : ( CD = child_1 )
        & ? [CD: child_d] : ( CD = child_1 )
        & ! [CD1: child_d,CD2: child_d] :
            ( ( d2child(CD1) = d2child(CD2) ) => ( CD1 = CD2 ) )
        & ! [A: adult] : ? [AD: adult_d] : ( A = d2adult(AD) )
        & ! [AD: adult_d] : ( AD = adult_1 )
        & ? [AD: adult_d] : ( AD = adult_1 )
        & ! [AD1: adult_d,AD2: adult_d] :
            ( ( d2adult(AD1) = d2adult(AD2) ) => ( AD1 = AD2 ) ) ))

Interpret functions

tff(people_mappings,interpretation-mappings,
    ( $in_world(w1,
        ( ( charly = d2child(child_1) )
        & ( agatha = d2adult(adult_1) )
        & ( serves(d2adult(adult_1)) = d2child(child_1) )

Interpret predicates

        & ~ quiet(d2child(child_1))
        & ~ sleepy(d2adult(adult_1))
        & peaceful(d2child(child_1))
        & rains ))

Quantification for Compaction

Avoid repetition

tff(people_domains,interpretation-domains,
    ( $in_world(w1,

        ( ! [C: child] : ? [CD: child_d] : ( C = d2child(CD) )
        & ! [CD: child_d] : ( CD = child_1 )
        & ? [CD: child_d] : ( CD = child_1 )
        & ! [CD1: child_d,CD2: child_d] :
            ( ( d2child(CD1) = d2child(CD2) ) => ( CD1 = CD2 ) )
        & ! [A: adult] : ? [AD: adult_d] : ( A = d2adult(AD) )
        & ! [AD: adult_d] : ( AD = adult_1 )
        & ? [AD: adult_d] : ( AD = adult_1 )
        & ! [AD1: adult_d,AD2: adult_d] :
            ( ( d2adult(AD1) = d2adult(AD2) ) => ( AD1 = AD2 ) ) ))

    & $in_world(w2,

tff(people_mappings,interpretation-mappings,
    ( $in_world(w1,

        ( ( charly = d2child(child_1) )
        & ( agatha = d2adult(adult_1) )
        & ( serves(d2adult(adult_1)) = d2child(child_1) )
        & ~ quiet(d2child(child_1))
        & ~ sleepy(d2adult(adult_1))
        & peaceful(d2child(child_1))
        & rains ))

    & $in_world(w2,

With quantification

tff(people_domains,interpretation-domains,

    ! [W: $world] :
      $in_world(W,
        ( ! [C: child] : ? [CD: child_d] : C = d2child(CD)
        & ! [CD: child_d] : CD = child_1
        & ? [CD: child_d] : CD = child_1
        & ! [CD1: child_d,CD2: child_d] :
            ( d2child(CD1) = d2child(CD2) => CD1 = CD2 )
        & ! [A: adult] : ? [AD: adult_d] : A = d2adult(AD)
        & ! [AD: adult_d] : AD = adult_1
        & ? [AD: adult_d] : AD = adult_1
        & ! [AD1: adult_d,AD2: adult_d] :
            ( d2adult(AD1) = d2adult(AD2) => AD1 = AD2 ) )) ).


tff(charly_mappings,interpretation-mappings,

    ! [W: $world] :
      $in_world(W,
        ( charly = d2child(child_1) 
        & agatha = d2adult(adult_1)
        & serves(d2adult(adult_1)) = d2child(child_1)
        & ~ quiet(d2child(child_1))
        & ~ sleepy(d2adult(adult_1))
        & peaceful(d2child(child_1))
        & rains)) ).

Complete Examples

Sleepy Children Finite worlds, Finite domains

Sleepy Children		Finite-Finite Countermodel
%------------------------------------------------------------------------------ tff(semantics,logic, $alethic_modal == [ $domains == $constant, $designation == $rigid, $terms == $local, $modalities == $modal_system_K ] ). tff(child_type,type, child: $tType ). tff(adult_type,type, adult: $tType ). tff(agatha_decl,type, agatha: adult ). tff(charly_decl,type, charly: child ). tff(quiet_decl,type, quiet: child > $o ). tff(sleepy_decl,type, sleepy: adult > $o ). tff(peaceful_decl,type, peaceful: child > $o ). tff(serves_decl,type, serves: adult > child ). tff(rains_decl,type, rains: $o ). tff(a1,axiom, ! [C: child] : ~ ( ~quiet(C) & ? [A: adult] : sleepy(A) ) ). tff(a2,axiom, ( ( rains & ? [C: child] : quiet(C) ) => ! [C: child] : ~peaceful(C) ) ). tff(a3,axiom, ( peaceful(charly) \| ( ~quiet(charly) & quiet(serves(agatha)) ) ) ). tff(a4,axiom, ~quiet(charly) => ! [C: child] : ~quiet(C) ). tff(a5,axiom, {$necessary} @ ( peaceful(charly) => rains ) ). tff(c,conjecture, {$possible} @ (~ rains) ). %------------------------------------------------------------------------------		%------------------------------------------------------------------------------ tff(semantics,logic, $alethic_modal == [ $domains == $constant, $designation == $rigid, $terms == $local, $modalities == $modal_system_M ] ). tff(child_type,type, child: $tType ). tff(adult_type,type, adult: $tType ). tff(agatha_decl,type, agatha: adult ). tff(charly_decl,type, charly: child ). tff(quiet_decl,type, quiet: child > $o ). tff(sleepy_decl,type, sleepy: adult > $o ). tff(peaceful_decl,type, peaceful: child > $o ). tff(serves_decl,type, serves: adult > child ). tff(rains_decl,type, rains: $o ). tff(child_d_decl,type, child_d: $tType). tff(adult_d_decl,type, adult_d: $tType). tff(child_1_decl,type, child_1: child_d). tff(adult_1_decl,type, adult_1: adult_d). tff(d2child_decl,type, d2child: child_d > child). tff(d2adult_decl,type, d2adult: adult_d > adult). tff(w1_decl,type, w1: $world ). tff(w2_decl,type, w2: $world ). tff(w3_decl,type, w3: $world ). tff(people_worlds,interpretation-worlds, ( ! [W: $world] : ( ( W = w1 ) \| ( W = w2 ) \| ( W = w3 ) ) & $distinct(w1,w2,w3) & ( $local_world = w1 ) & $accessible_world(w1,w1) & $accessible_world(w2,w2) & $accessible_world(w1,w2) & $accessible_world(w2,w3) & $accessible_world(w3,w1) & ~ $accessible_world(w1,w3) & ~ $accessible_world(w2,w1) & ~ $accessible_world(w3,w2) & ~ $accessible_world(w3,w3) ) ). %----All worlds have the same Tarskian interpretation. tff(people_domains,interpretation-domains, ( $in_world(w1, ( ! [C: child] : ? [CD: child_d] : ( C = d2child(CD) ) & ! [CD: child_d] : ( CD = child_1 ) & ? [CD: child_d] : ( CD = child_1 ) & ! [CD1: child_d,CD2: child_d] : ( ( d2child(CD1) = d2child(CD2) ) => ( CD1 = CD2 ) ) & ! [A: adult] : ? [AD: adult_d] : ( A = d2adult(AD) ) & ! [AD: adult_d] : ( AD = adult_1 ) & ? [AD: adult_d] : ( AD = adult_1 ) & ! [AD1: adult_d,AD2: adult_d] : ( ( d2adult(AD1) = d2adult(AD2) ) => ( AD1 = AD2 ) ) )) & $in_world(w2, ( ! [C: child] : ? [CD: child_d] : ( C = d2child(CD) ) & ! [CD: child_d] : ( CD = child_1 ) & ? [CD: child_d] : ( CD = child_1 ) & ! [CD1: child_d,CD2: child_d] : ( ( d2child(CD1) = d2child(CD2) ) => ( CD1 = CD2 ) ) & ! [A: adult] : ? [AD: adult_d] : ( A = d2adult(AD) ) & ! [AD: adult_d] : ( AD = adult_1 ) & ? [AD: adult_d] : ( AD = adult_1 ) & ! [AD1: adult_d,AD2: adult_d] : ( ( d2adult(AD1) = d2adult(AD2) ) => ( AD1 = AD2 ) ) )) & $in_world(w3, ( ! [C: child] : ? [CD: child_d] : ( C = d2child(CD) ) & ! [CD: child_d] : ( CD = child_1 ) & ? [CD: child_d] : ( CD = child_1 ) & ! [CD1: child_d,CD2: child_d] : ( ( d2child(CD1) = d2child(CD2) ) => ( CD1 = CD2 ) ) & ! [A: adult] : ? [AD: adult_d] : ( A = d2adult(AD) ) & ! [AD: adult_d] : ( AD = adult_1 ) & ? [AD: adult_d] : ( AD = adult_1 ) & ! [AD1: adult_d,AD2: adult_d] : ( ( d2adult(AD1) = d2adult(AD2) ) => ( AD1 = AD2 ) ) )) ) ). tff(people_mappings,interpretation-mappings, ( $in_world(w1, ( ( charly = d2child(child_1) ) & ( agatha = d2adult(adult_1) ) & ( serves(d2adult(adult_1)) = d2child(child_1) ) & ~ quiet(d2child(child_1)) & ~ sleepy(d2adult(adult_1)) & peaceful(d2child(child_1)) & rains )) & $in_world(w2, ( ( charly = d2child(child_1) ) & ( agatha = d2adult(adult_1) ) & ( serves(d2adult(adult_1)) = d2child(child_1) ) & ~ quiet(d2child(child_1)) & ~ sleepy(d2adult(adult_1)) & peaceful(d2child(child_1)) & rains )) & $in_world(w3, ( ( charly = d2child(child_1) ) & ( agatha = d2adult(adult_1) ) & ( serves(d2adult(adult_1)) = d2child(child_1) ) & ~ quiet(d2child(child_1)) & ~ sleepy(d2adult(adult_1)) & peaceful(d2child(child_1)) & rains )) ) ). %------------------------------------------------------------------------------

Sleepy Children

Finite-Finite Countermodel

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

tff(child_type,type,    child: $tType ).
tff(adult_type,type,    adult: $tType ).
tff(agatha_decl,type,   agatha: adult ).
tff(charly_decl,type,   charly: child ).
tff(quiet_decl,type,    quiet: child > $o ).
tff(sleepy_decl,type,   sleepy: adult > $o ).
tff(peaceful_decl,type, peaceful: child > $o ).
tff(serves_decl,type,   serves: adult > child ).
tff(rains_decl,type,    rains: $o ).

tff(a1,axiom,
    ! [C: child] :
      ~ ( ~quiet(C) & ? [A: adult] : sleepy(A) ) ).

tff(a2,axiom,
    ( ( rains & ? [C: child] : quiet(C) )
   => ! [C: child] : ~peaceful(C) ) ).

tff(a3,axiom,
    ( peaceful(charly)
    | ( ~quiet(charly) & quiet(serves(agatha)) ) ) ).

tff(a4,axiom,
    ~quiet(charly) => ! [C: child] : ~quiet(C) ).

tff(a5,axiom,
    {$necessary} @ ( peaceful(charly) => rains ) ).

tff(c,conjecture,
    {$possible} @ (~ rains) ).
%------------------------------------------------------------------------------

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

tff(child_type,type,    child: $tType ).
tff(adult_type,type,    adult: $tType ).
tff(agatha_decl,type,   agatha: adult ).
tff(charly_decl,type,   charly: child ).
tff(quiet_decl,type,    quiet: child > $o ).
tff(sleepy_decl,type,   sleepy: adult > $o ).
tff(peaceful_decl,type, peaceful: child > $o ).
tff(serves_decl,type,   serves: adult > child ).
tff(rains_decl,type,    rains: $o ).

tff(child_d_decl,type,  child_d: $tType).
tff(adult_d_decl,type,  adult_d: $tType).
tff(child_1_decl,type,  child_1: child_d).
tff(adult_1_decl,type,  adult_1: adult_d).
tff(d2child_decl,type,  d2child: child_d > child).
tff(d2adult_decl,type,  d2adult: adult_d > adult).

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

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

%----All worlds have the same Tarskian interpretation.
tff(people_domains,interpretation-domains,
    ( $in_world(w1,
        ( ! [C: child] : ? [CD: child_d] : ( C = d2child(CD) )
        & ! [CD: child_d] : ( CD = child_1 )
        & ? [CD: child_d] : ( CD = child_1 )
        & ! [CD1: child_d,CD2: child_d] :
            ( ( d2child(CD1) = d2child(CD2) ) => ( CD1 = CD2 ) )
        & ! [A: adult] : ? [AD: adult_d] : ( A = d2adult(AD) )
        & ! [AD: adult_d] : ( AD = adult_1 )
        & ? [AD: adult_d] : ( AD = adult_1 )
        & ! [AD1: adult_d,AD2: adult_d] :
            ( ( d2adult(AD1) = d2adult(AD2) ) => ( AD1 = AD2 ) ) ))
    & $in_world(w2,
        ( ! [C: child] : ? [CD: child_d] : ( C = d2child(CD) )
        & ! [CD: child_d] : ( CD = child_1 )
        & ? [CD: child_d] : ( CD = child_1 )
        & ! [CD1: child_d,CD2: child_d] :
            ( ( d2child(CD1) = d2child(CD2) ) => ( CD1 = CD2 ) )
        & ! [A: adult] : ? [AD: adult_d] : ( A = d2adult(AD) )
        & ! [AD: adult_d] : ( AD = adult_1 )
        & ? [AD: adult_d] : ( AD = adult_1 )
        & ! [AD1: adult_d,AD2: adult_d] :
            ( ( d2adult(AD1) = d2adult(AD2) ) => ( AD1 = AD2 ) ) ))
    & $in_world(w3,
        ( ! [C: child] : ? [CD: child_d] : ( C = d2child(CD) )
        & ! [CD: child_d] : ( CD = child_1 )
        & ? [CD: child_d] : ( CD = child_1 )
        & ! [CD1: child_d,CD2: child_d] :
            ( ( d2child(CD1) = d2child(CD2) ) => ( CD1 = CD2 ) )
        & ! [A: adult] : ? [AD: adult_d] : ( A = d2adult(AD) )
        & ! [AD: adult_d] : ( AD = adult_1 )
        & ? [AD: adult_d] : ( AD = adult_1 )
        & ! [AD1: adult_d,AD2: adult_d] :
            ( ( d2adult(AD1) = d2adult(AD2) ) => ( AD1 = AD2 ) ) )) ) ).

tff(people_mappings,interpretation-mappings,
    ( $in_world(w1,
        ( ( charly = d2child(child_1) )
        & ( agatha = d2adult(adult_1) )
        & ( serves(d2adult(adult_1)) = d2child(child_1) )
        & ~ quiet(d2child(child_1))
        & ~ sleepy(d2adult(adult_1))
        & peaceful(d2child(child_1))
        & rains ))
    & $in_world(w2,
        ( ( charly = d2child(child_1) )
        & ( agatha = d2adult(adult_1) )
        & ( serves(d2adult(adult_1)) = d2child(child_1) )
        & ~ quiet(d2child(child_1))
        & ~ sleepy(d2adult(adult_1))
        & peaceful(d2child(child_1))
        & rains ))
    & $in_world(w3,
        ( ( charly = d2child(child_1) )
        & ( agatha = d2adult(adult_1) )
        & ( serves(d2adult(adult_1)) = d2child(child_1) )
        & ~ quiet(d2child(child_1))
        & ~ sleepy(d2adult(adult_1))
        & peaceful(d2child(child_1))
        & rains )) ) ).
%------------------------------------------------------------------------------

Sleepy Children Compact

Sleepy Children		Compacted
%------------------------------------------------------------------------------ tff(semantics,logic, $alethic_modal == [ $domains == $constant, $designation == $rigid, $terms == $local, $modalities == $modal_system_M ] ). tff(child_type,type, child: $tType ). tff(adult_type,type, adult: $tType ). tff(agatha_decl,type, agatha: adult ). tff(charly_decl,type, charly: child ). tff(quiet_decl,type, quiet: child > $o ). tff(sleepy_decl,type, sleepy: adult > $o ). tff(peaceful_decl,type, peaceful: child > $o ). tff(serves_decl,type, serves: adult > child ). tff(rains_decl,type, rains: $o ). tff(child_d_decl,type, child_d: $tType). tff(adult_d_decl,type, adult_d: $tType). tff(child_1_decl,type, child_1: child_d). tff(adult_1_decl,type, adult_1: adult_d). tff(d2child_decl,type, d2child: child_d > child). tff(d2adult_decl,type, d2adult: adult_d > adult). tff(w1_decl,type, w1: $world ). tff(w2_decl,type, w2: $world ). tff(w3_decl,type, w3: $world ). tff(people_worlds,interpretation-worlds, ( ! [W: $world] : ( ( W = w1 ) \| ( W = w2 ) \| ( W = w3 ) ) & $distinct(w1,w2,w3) & ( $local_world = w1 ) & $accessible_world(w1,w1) & $accessible_world(w2,w2) & $accessible_world(w1,w2) & $accessible_world(w2,w3) & $accessible_world(w3,w1) & ~ $accessible_world(w1,w3) & ~ $accessible_world(w2,w1) & ~ $accessible_world(w3,w2) & ~ $accessible_world(w3,w3) ) ). %----All worlds have the same Tarskian interpretation. tff(people_domains,interpretation-domains, ( $in_world(w1, ( ! [C: child] : ? [CD: child_d] : ( C = d2child(CD) ) & ! [CD: child_d] : ( CD = child_1 ) & ? [CD: child_d] : ( CD = child_1 ) & ! [CD1: child_d,CD2: child_d] : ( ( d2child(CD1) = d2child(CD2) ) => ( CD1 = CD2 ) ) & ! [A: adult] : ? [AD: adult_d] : ( A = d2adult(AD) ) & ! [AD: adult_d] : ( AD = adult_1 ) & ? [AD: adult_d] : ( AD = adult_1 ) & ! [AD1: adult_d,AD2: adult_d] : ( ( d2adult(AD1) = d2adult(AD2) ) => ( AD1 = AD2 ) ) )) & $in_world(w2, ( ! [C: child] : ? [CD: child_d] : ( C = d2child(CD) ) & ! [CD: child_d] : ( CD = child_1 ) & ? [CD: child_d] : ( CD = child_1 ) & ! [CD1: child_d,CD2: child_d] : ( ( d2child(CD1) = d2child(CD2) ) => ( CD1 = CD2 ) ) & ! [A: adult] : ? [AD: adult_d] : ( A = d2adult(AD) ) & ! [AD: adult_d] : ( AD = adult_1 ) & ? [AD: adult_d] : ( AD = adult_1 ) & ! [AD1: adult_d,AD2: adult_d] : ( ( d2adult(AD1) = d2adult(AD2) ) => ( AD1 = AD2 ) ) )) & $in_world(w3, ( ! [C: child] : ? [CD: child_d] : ( C = d2child(CD) ) & ! [CD: child_d] : ( CD = child_1 ) & ? [CD: child_d] : ( CD = child_1 ) & ! [CD1: child_d,CD2: child_d] : ( ( d2child(CD1) = d2child(CD2) ) => ( CD1 = CD2 ) ) & ! [A: adult] : ? [AD: adult_d] : ( A = d2adult(AD) ) & ! [AD: adult_d] : ( AD = adult_1 ) & ? [AD: adult_d] : ( AD = adult_1 ) & ! [AD1: adult_d,AD2: adult_d] : ( ( d2adult(AD1) = d2adult(AD2) ) => ( AD1 = AD2 ) ) )) ) ). tff(people_mappings,interpretation-mappings, ( $in_world(w1, ( ( charly = d2child(child_1) ) & ( agatha = d2adult(adult_1) ) & ( serves(d2adult(adult_1)) = d2child(child_1) ) & ~ quiet(d2child(child_1)) & ~ sleepy(d2adult(adult_1)) & peaceful(d2child(child_1)) & rains )) & $in_world(w2, ( ( charly = d2child(child_1) ) & ( agatha = d2adult(adult_1) ) & ( serves(d2adult(adult_1)) = d2child(child_1) ) & ~ quiet(d2child(child_1)) & ~ sleepy(d2adult(adult_1)) & peaceful(d2child(child_1)) & rains )) & $in_world(w3, ( ( charly = d2child(child_1) ) & ( agatha = d2adult(adult_1) ) & ( serves(d2adult(adult_1)) = d2child(child_1) ) & ~ quiet(d2child(child_1)) & ~ sleepy(d2adult(adult_1)) & peaceful(d2child(child_1)) & rains )) ) ). %------------------------------------------------------------------------------		[an error occurred while processing this directive]

Sleepy Children

Compacted

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

tff(child_type,type,    child: $tType ).
tff(adult_type,type,    adult: $tType ).
tff(agatha_decl,type,   agatha: adult ).
tff(charly_decl,type,   charly: child ).
tff(quiet_decl,type,    quiet: child > $o ).
tff(sleepy_decl,type,   sleepy: adult > $o ).
tff(peaceful_decl,type, peaceful: child > $o ).
tff(serves_decl,type,   serves: adult > child ).
tff(rains_decl,type,    rains: $o ).

tff(child_d_decl,type,  child_d: $tType).
tff(adult_d_decl,type,  adult_d: $tType).
tff(child_1_decl,type,  child_1: child_d).
tff(adult_1_decl,type,  adult_1: adult_d).
tff(d2child_decl,type,  d2child: child_d > child).
tff(d2adult_decl,type,  d2adult: adult_d > adult).

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

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

%----All worlds have the same Tarskian interpretation.
tff(people_domains,interpretation-domains,
    ( $in_world(w1,
        ( ! [C: child] : ? [CD: child_d] : ( C = d2child(CD) )
        & ! [CD: child_d] : ( CD = child_1 )
        & ? [CD: child_d] : ( CD = child_1 )
        & ! [CD1: child_d,CD2: child_d] :
            ( ( d2child(CD1) = d2child(CD2) ) => ( CD1 = CD2 ) )
        & ! [A: adult] : ? [AD: adult_d] : ( A = d2adult(AD) )
        & ! [AD: adult_d] : ( AD = adult_1 )
        & ? [AD: adult_d] : ( AD = adult_1 )
        & ! [AD1: adult_d,AD2: adult_d] :
            ( ( d2adult(AD1) = d2adult(AD2) ) => ( AD1 = AD2 ) ) ))
    & $in_world(w2,
        ( ! [C: child] : ? [CD: child_d] : ( C = d2child(CD) )
        & ! [CD: child_d] : ( CD = child_1 )
        & ? [CD: child_d] : ( CD = child_1 )
        & ! [CD1: child_d,CD2: child_d] :
            ( ( d2child(CD1) = d2child(CD2) ) => ( CD1 = CD2 ) )
        & ! [A: adult] : ? [AD: adult_d] : ( A = d2adult(AD) )
        & ! [AD: adult_d] : ( AD = adult_1 )
        & ? [AD: adult_d] : ( AD = adult_1 )
        & ! [AD1: adult_d,AD2: adult_d] :
            ( ( d2adult(AD1) = d2adult(AD2) ) => ( AD1 = AD2 ) ) ))
    & $in_world(w3,
        ( ! [C: child] : ? [CD: child_d] : ( C = d2child(CD) )
        & ! [CD: child_d] : ( CD = child_1 )
        & ? [CD: child_d] : ( CD = child_1 )
        & ! [CD1: child_d,CD2: child_d] :
            ( ( d2child(CD1) = d2child(CD2) ) => ( CD1 = CD2 ) )
        & ! [A: adult] : ? [AD: adult_d] : ( A = d2adult(AD) )
        & ! [AD: adult_d] : ( AD = adult_1 )
        & ? [AD: adult_d] : ( AD = adult_1 )
        & ! [AD1: adult_d,AD2: adult_d] :
            ( ( d2adult(AD1) = d2adult(AD2) ) => ( AD1 = AD2 ) ) )) ) ).

tff(people_mappings,interpretation-mappings,
    ( $in_world(w1,
        ( ( charly = d2child(child_1) )
        & ( agatha = d2adult(adult_1) )
        & ( serves(d2adult(adult_1)) = d2child(child_1) )
        & ~ quiet(d2child(child_1))
        & ~ sleepy(d2adult(adult_1))
        & peaceful(d2child(child_1))
        & rains ))
    & $in_world(w2,
        ( ( charly = d2child(child_1) )
        & ( agatha = d2adult(adult_1) )
        & ( serves(d2adult(adult_1)) = d2child(child_1) )
        & ~ quiet(d2child(child_1))
        & ~ sleepy(d2adult(adult_1))
        & peaceful(d2child(child_1))
        & rains ))
    & $in_world(w3,
        ( ( charly = d2child(child_1) )
        & ( agatha = d2adult(adult_1) )
        & ( serves(d2adult(adult_1)) = d2child(child_1) )
        & ~ quiet(d2child(child_1))
        & ~ sleepy(d2adult(adult_1))
        & peaceful(d2child(child_1))
        & rains )) ) ).
%------------------------------------------------------------------------------

[an error occurred while processing this directive]