%------------------------------------------------------------------------------
%----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_of(john) = f ).
fof(someone_got_an_a,axiom,
? [H] :
( human(H)
& grade_of(H) = a ) ).
fof(distinct_grades,axiom,
a != f ).
fof(grades_not_human,axiom,
! [G] : ~ human(grade_of(G)) ).
fof(equality_lost,conjecture,
! [H1,H2] :
( ( human(H1)
& human(H2)
& created_equal(H1,H2) )
<=> H1 = H2 ) ).
%------------------------------------------------------------------------------
fof(equality_lost,interpretation,
( ! [X] : ( X = "a" | X = "f" | X = "john" | X = "gotA")
Note the use of "quoted terms" that are known to be distinct.
& ( a = "a"
& f = "f"
& john = "john"
& grade_of("a") = "a"
& grade_of("f") = "a"
& grade_of("john") = "f"
& grade_of("gotA") = "a" )
Note the interpretation of meaningless terms.
& ( ~ 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 the interpretation of meaningless atoms.
%------------------------------------------------------------------------------
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(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 ).... and add type promotion functions ...
tff(d2human_decl,type, d2human: d_human > human ). tff(d2cat_decl,type, d2cat: d_cat > 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_garfield)
& 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)) ) ).
%------------------------------------------------------------------------------
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 ).
%----Types of the domain elements
tff(d_jon_decl,type, d_jon: human ).
tff(d_garfield_decl,type, d_garfield: cat ).
tff(d_arlene_decl,type, d_arlene: cat ).
tff(d_nermal_decl,type, d_nermal: cat ).
tff(garfield,interpretation,
%----The human domain elements are {d_jon}
( ( ! [DH: human] : ( DH = d_jon )
%----The cat domain elements are {d_garfield,d_arlene,d_nermal}
& ! [DC: cat]:
( DC = d_garfield | DC = d_arlene | DC = d_nermal )
& $distinct(d_garfield,d_arlene,d_nermal) )
%----Interpret functions
& ( jon = d_jon
& garfield = d_garfield
& arlene = d_arlene
& nermal = d_nermal
& loves(d_garfield) = d_garfield
& loves(d_arlene) = d_garfield
& loves(d_nermal) = d_garfield )
%----Interpret predicates
& ( owns(d_jon,d_garfield)
& ~ owns(d_jon,d_arlene)
& ~ owns(d_jon,d_nermal) ) ) ).
%------------------------------------------------------------------------------
| Egalitarian Students | Finite Countermodel | |
|---|---|---|
%------------------------------------------------------------------------------
%----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_of(john) = f ).
fof(someone_got_an_a,axiom,
? [H] :
( human(H)
& grade_of(H) = a ) ).
fof(distinct_grades,axiom,
a != f ).
fof(grades_not_human,axiom,
! [G] : ~ human(grade_of(G)) ).
fof(equality_lost,conjecture,
! [H1,H2] :
( ( human(H1)
& human(H2)
& created_equal(H1,H2) )
<=> H1 = H2 ) ).
%------------------------------------------------------------------------------
|
%------------------------------------------------------------------------------
fof(equality_lost,interpretation,
( ! [X] : ( X = "a" | X = "f" | X = "john" | X = "gotA")
& ( a = "a"
& f = "f"
& john = "john"
& grade_of("a") = "a"
& grade_of("f") = "a"
& grade_of("john") = "f"
& grade_of("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") ) ) ).
%------------------------------------------------------------------------------
|
| Jon Owns Garfield's Lovers | Finite Countermodel | |
|---|---|---|
%------------------------------------------------------------------------------
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 ).
%----Types of the domains
tff(d_human_type,type, d_human: $tType ).
tff(d_cat_type,type, d_cat: $tType ).
%----Types of the domain elements
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 ).
%----Types of the promotion functions
tff(d2human_decl,type, d2human: d_human > human ).
tff(d2cat_decl,type, d2cat: d_cat > cat ).
tff(garfield,interpretation,
%----The domain for human is d_human, with elements {d_jon}
( ! [H: human] : ? [DH: d_human] : H = d2human(DH)
& ! [DH: d_human] : ( DH = d_jon )
%----The type-promoter is a bijection
& ! [DH1: d_human,DH2: d_human] :
( d2human(DH1) = d2human(DH2) => DH1 = DH2 )
%----The domain for cat is d_cat, with distinct elements
%----{d_garfield,d_arlene,d_nermal}
& ! [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 )
%----Interpret terms via the type-promoted domain
& jon = d2human(d_jon)
& garfield = d2cat(d_garfield)
& arlene = d2cat(d_arlene)
& nermal = d2cat(d_nermal)
& loves(d2cat(d_garfield)) = d2cat(d_garfield)
& loves(d2cat(d_arlene)) = d2cat(d_garfield)
& loves(d2cat(d_nermal)) = d2cat(d_garfield)
%----Interpret atoms as true or false
& owns(d2human(d_jon),d2cat(d_garfield))
& ~ owns(d2human(d_jon),d2cat(d_arlene))
& ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ).
%------------------------------------------------------------------------------
|