%------------------------------------------------------------------------------ %----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.
%------------------------------------------------------------------------------ %----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.
%------------------------------------------------------------------------------ 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.
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.
%------------------------------------------------------------------------------ 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.
%------------------------------------------------------------------------------ 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.
%------------------------------------------------------------------------------ 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.
%------------------------------------------------------------------------------ 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.
For example ...
tff(myI_domain,domain, ! [X: $i] : ( X = "face" | X = "stickman" ) ).
tff(myI_functions,functors, ( geoff = "face" & brotherOf("face") = "stickman" & brotherOf("stickman") = "face" ) ).
tff(myI_predicates,predicates, ( ~ taller("face","face") & ~ taller("face","stickman") & taller("stickman","face") & ~ taller("stickman","stickman") ) ).
Proof that
if φ_{Ι} ⊨ φ then Ι ⊨ φ