| 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 )) ) ).
%------------------------------------------------------------------------------
|
| Rotten Fruit | Finite-Finite Countermodel | |
|---|---|---|
%------------------------------------------------------------------------------
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(w1_decl,type,w1: $world).
tff(w2_decl,type,w2: $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-worlds,
( ! [W: $world] : ( W = w1 | W = w2 )
& $distinct(w1,w2)
& $local_world = w1
& $accessible_world(w1,w1)
& $accessible_world(w2,w2)
& $accessible_world(w1,w2)
& ~ $accessible_world(w2,w1) ) ).
tff(fruity_domains,interpretation-domains,
! [W: $world] :
$in_world(W,
( ! [F: fruit] : ? [DF: d_fruit] : F = d2fruit(DF)
& ! [DF: d_fruit] : ( DF = d_apple | DF = d_banana )
& $distinct(d_apple,d_banana)
& ? [DP: d_fruit] : ( DP = d_apple )
& ? [DP: d_fruit] : ( DP = d_banana )
& ! [DF1: d_fruit,DF2: d_fruit] :
( d2fruit(DF1) = d2fruit(DF2) => DF1 = DF2 ) )) ).
tff(fruity_healthy_mappings,interpretation-mappings,
! [W: $world] :
$in_world(W,
( apple = d2fruit(d_apple)
& banana = d2fruit(d_banana)
& healthy(d2fruit(d_apple))
& healthy(d2fruit(d_banana)) )) ).
tff(fruity_rotten_mappings,interpretation-mappings,
( $in_world(w1,
( ~ rotten(d2fruit(d_apple))
& rotten(d2fruit(d_banana)) ))
& $in_world(w2,
( ~ rotten(d2fruit(d_apple))
& ~ rotten(d2fruit(d_banana)) )) ) ).
%------------------------------------------------------------------------------
|
| Tossing Heads | Finite-Infinite Countermodel | |
|---|---|---|
%------------------------------------------------------------------------------
tff(simple_spec,logic,
$alethic_modal ==
[ $domains == $constant,
$designation == $rigid,
$terms == $local,
$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 ==
[ $domains == $constant,
$designation == $rigid,
$terms == $local,
$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 ) )
& $distinct(w1,w2)
& $local_world = w1
& $accessible_world(w1,w1)
& $accessible_world(w2,w2)
& $accessible_world(w1,w2)
& ~ $accessible_world(w2,w1) )
& $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))) ) ) ) ) ) ) ).
%------------------------------------------------------------------------------
|
| Staying Alive | Infinite-Finite Model | |
|---|---|---|
%------------------------------------------------------------------------------
tff(simple_spec,logic,
$alethic_modal ==
[ $domains == $constant,
$designation == $rigid,
$terms == $local,
$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 ==
[ $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_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) ) ) ) ) ) ) ) ).
%------------------------------------------------------------------------------
|
| People Like People | Infinite-Infinite Model | |
|---|---|---|
%------------------------------------------------------------------------------
tff(simple_spec,logic,
$alethic_modal ==
[ $domains == $varying,
$designation == $flexible,
$terms == $local,
$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 ==
[ $domains == $varying,
$designation == $flexible,
$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_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) and all other worlds
& ! [I: $int] :
( $greatereq(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 ) ) ) ) ) ) ).
%------------------------------------------------------------------------------
|