Tarskian Interpretations

In FOF

• The Egalitarian student problem

  %------------------------------------------------------------------------------
  %----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 ) ).
  %------------------------------------------------------------------------------
  
       

• New role interpretation

  fof(equality_lost,interpretation, 

• Specify the domain

      ( ! [X] : ( X = "a" | X = "f" | X = "john" | X = "gotA") 

  Note the use of "quoted terms" that are known to be distinct.
• Interpret functions

      & ( 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.
• Interpret predicates

      & ( ~ 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.

In TFF (and beyond)

• The Garfield problem

  %------------------------------------------------------------------------------
  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) ) ).
  %------------------------------------------------------------------------------
  
       

• Keep problem types

  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 ). 

• Declare new domain types to declare domain elements

  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 ). 

• New role interpretation

  tff(garfield,interpretation, 

• Specify domains

      ( ! [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 ) 

• Interpret functions (using type promoted domain elements)

      & 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 predicates

      & owns(d2human(d_jon),d2cat(d_garfield))
      & ~ owns(d2human(d_jon),d2cat(d_arlene))
      & ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ). 

• You can reuse problem types and get confused

  %------------------------------------------------------------------------------
  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) ) ) ).
  %------------------------------------------------------------------------------
  
       

Complete Examples

Egalitarian Students

%------------------------------------------------------------------------------
%----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

%------------------------------------------------------------------------------
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)) ) ).
%------------------------------------------------------------------------------