tff(human_type,type, human: $tType ). tff(cat_type,type, cat: $tType ). tff(jon_decl,type, jon: human ). tff(garfield_decl,type, garfield: cat ). tff(arlene_decl,type, arlene: cat ). tff(nermal_decl,type, nermal: cat ). tff(loves_decl,type, loves: cat > cat ). tff(owns_decl,type, owns: ( human * cat ) > $o ).
tff(d_human_type,type, d_human: $tType ). tff(d_cat_type,type, d_cat: $tType ). tff(d2human_decl,type, d2human: d_human > human ). tff(d2cat_decl,type, d2cat: d_cat > cat ).
tff(d_jon_decl,type, d_jon: d_human ). tff(d_garfield_decl,type, d_garfield: d_cat ). tff(d_arlene_decl,type, d_arlene: d_cat ). tff(d_nermal_decl,type, d_nermal: d_cat ).
tff(garfield,interpretation,
( ! [H: human] : ? [DH: d_human] : H = d2human(DH)
& ! [DH: d_human] : ( DH = d_jon )
& ! [DH1: d_human,DH2: d_human] :
( d2human(DH1) = d2human(DH2) => DH1 = DH2 )
& ! [C: cat] : ? [DC: d_cat] : C = d2cat(DC)
& ! [DC: d_cat]:
( DC = d_garfield | DC = d_arlene | DC = d_nermal )
& $distinct(d_garfield,d_arlene,d_nermal)
& ! [DC1: d_cat,DC2: d_cat] :
( d2cat(DC1) = d2cat(DC2) => DC1 = DC2 ) )
( jon = d2human(d_jon) & garfield = d2cat(d_garfield) & arlene = d2cat(d_arlene) & nermal = d2cat(d_nermal) & loves(d2cat(d_garfield)) = d2cat(d_garfiel)d & loves(d2cat(d_arlene)) = d2cat(d_garfield) & loves(d2cat(d_nermal)) = d2cat(d_garfield)) )
( owns(d2human(d_jon),d2cat(d_garfield)) & ~ owns(d2human(d_jon),d2cat(d_arlene)) & ~ owns(d2human(d_jon),d2cat(d_nermal)) )
| Jon Owns Garfield's Lovers | Finite Countermodel - Compact |
|---|---|
%------------------------------------------------------------------------------
tff(human_type,type, human: $tType ).
tff(cat_type,type, cat: $tType ).
tff(jon_decl,type, jon: human ).
tff(garfield_decl,type, garfield: cat ).
tff(arlene_decl,type, arlene: cat ).
tff(nermal_decl,type, nermal: cat ).
tff(loves_decl,type, loves: cat > cat ).
tff(owns_decl,type, owns: ( human * cat ) > $o ).
tff(only_jon,axiom, ! [H: human] : H = jon ).
tff(only_garfield_and_arlene_and_nermal,axiom,
! [C: cat] :
( C = garfield | C = arlene | C = nermal ) ).
tff(distinct_cats,axiom,
( garfield != arlene & arlene != nermal
& nermal != garfield ) ).
tff(jon_owns_garfield_not_arlene,axiom,
( owns(jon,garfield) & ~ owns(jon,arlene) ) ).
tff(all_cats_love_garfield,axiom,
! [C: cat] : ( loves(C) = garfield ) ).
tff(jon_owns_garfields_lovers,conjecture,
! [C: cat] :
( ( loves(C) = garfield & C != arlene )
=> owns(jon,C) ) ).
%------------------------------------------------------------------------------
|
%------------------------------------------------------------------------------
tff(human_type,type, human: $tType ).
tff(cat_type,type, cat: $tType ).
tff(jon_decl,type, jon: human ).
tff(garfield_decl,type, garfield: cat ).
tff(arlene_decl,type, arlene: cat ).
tff(nermal_decl,type, nermal: cat ).
tff(loves_decl,type, loves: cat > cat ).
tff(owns_decl,type, owns: ( human * cat ) > $o ).
tff(d_human_type,type, d_human: $tType ).
tff(d_cat_type,type, d_cat: $tType ).
tff(d2human_decl,type, d2human: d_human > human ).
tff(d2cat_decl,type, d2cat: d_cat > cat ).
tff(d_jon_decl,type, d_jon: d_human ).
tff(d_garfield_decl,type, d_garfield: d_cat ).
tff(d_arlene_decl,type, d_arlene: d_cat ).
tff(d_nermal_decl,type, d_nermal: d_cat ).
tff(garfield_domain_human,interpretation-domain(human,d_human),
( ! [H: human] : ? [DH: d_human] : H = d2human(DH)
& ! [DH: d_human] : ( DH = d_jon )
& ! [DH1: d_human,DH2: d_human] :
( d2human(DH1) = d2human(DH2) => DH1 = DH2 ) ) ).
tff(garfield_domain_cat,interpretation-domain(cat,d_cat),
( ! [C: cat] : ? [DC: d_cat] : C = d2cat(DC)
& ! [DC: d_cat]:
( DC = d_garfield | DC = d_arlene | DC = d_nermal )
& $distinct(d_garfield,d_arlene,d_nermal)
& ! [DC1: d_cat,DC2: d_cat] :
( d2cat(DC1) = d2cat(DC2) => DC1 = DC2 ) ) ).
tff(garfield_mapping_jon,interpretation-mapping(jon,d_human),
jon = d2human(d_jon) ).
tff(garfield_mapping_cats,interpretation-mapping,
( garfield = d2cat(d_garfield)
& arlene = d2cat(d_arlene)
& nermal = d2cat(d_nermal) ) ).
tff(garfield_mapping_loves,interpretation-mapping(loves,d_cat),
! [DC: d_cat] : ( loves(d2cat(DC)) = d2cat(d_garfield) ) ).
tff(garfield_mapping_owns,interpretation-mapping(owns,$o),
( owns(d2human(d_jon),d2cat(d_garfield))
& ~ owns(d2human(d_jon),d2cat(d_arlene))
& ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ).
%------------------------------------------------------------------------------
|
| Descendants Play the Peano | Infinite Term Model |
|---|---|
%------------------------------------------------------------------------------
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) ).
%------------------------------------------------------------------------------
|
%------------------------------------------------------------------------------
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) )
& ! [I: peano] : ( I = zero | ? [P: peano] : I = s(P) )
%----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 Peano numbers
& ( 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) ) ) ) ).
%------------------------------------------------------------------------------
|
| Descendants Count Forever | Infinite Integer Model |
|---|---|
%------------------------------------------------------------------------------
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) ).
%------------------------------------------------------------------------------
|
%------------------------------------------------------------------------------
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] : P = int2person(I)
%----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) ) ) ).
%------------------------------------------------------------------------------
|