Typed Higher-order Form

Typed Higher-order Form (THF)

• Curried types, lambda terms, application, connective terms, description binders
• Henkin semantics with choice (thus also extensionality)

Monomorphic THF (TH0)

• Types ... TF0, type signatures
• Type signatures ... types
• ATP systems ... agsyHOL, cvc5, Satallax, Vampire, etc.
• Example (as a plain file)

  thf(dog_type,type,       dog: $tType ).      thf(human_type,type,     human: $tType ).
  thf(odie_decl,type,      odie: dog ).        thf(jon_decl,type,       jon: human ).
  
  thf(owner_of_decl,type,  owner_of: dog > human ).
  thf(owns_decl,type,      owns: human > dog > $o ).
  thf(bit_decl,type,       bit: dog > human > $int > $o ).
  thf(hates_decl,type,     hates: human > human > $o ).
  thf(feeds_decl,type,     feeds: human > dog > $o ).
  thf(chases_decl,type,    chases: human > dog > $o ).
  thf(says_decl,type,      says: human > $o > $o ).
  
  thf(owns_defn,definition,
      ( owns = ( ^ [H: human,D: dog] : ( H = ( owner_of @ D ) ) ) ) ).
  
  thf(jon_owns_odie,axiom,                     thf(odie_bit_jon_twice,axiom,
      owns @ jon @ odie ).                         bit @ odie @ jon @ 2 ).
  
  thf(hate_the_multi_biter_dog,axiom,          thf(feed_the_non_biter_dog,axiom,
      ! [D: dog,H: human,N: $int] :                ! [D: dog,H: human] :
        ( ( ~ ( owns @ H @ D )                       $ite(
          & ( bit @ D @ H @ N )                        ? [N: $int] :
          & ( $greater @ N @ 1 ) )                       ( ( bit @ D @ H @ N )
       => ( hates @ H @ ( owner_of @ D ) ) ) ).          & ( $greater @ N @ 0 ) ),
                                                       chases @ H @ D,
  thf(jon_says_a_dog_bit_him_twice,axiom,              feeds @ H @ D) ).
      ? [D: dog] :
        ( ( D != odie )                        thf(jon_says_truth,axiom,
        & (~ ( owns @ jon @ D ))                   ! [S: $o] :
        & ( says @ jon @                             ( ( says @ jon @ S )
            ( bit @ D @ jon @ 2 ) ) ) ).            => S ) ).
  
  thf(jon_chases_and_feels,conjecture,
      ? [D:dog,H: human,F: human > human > $o] :
        ( ( chases @ jon @ D )
        & ( H != jon )
        & ( F @ jon @ H ) ) ).
  

Polymorphic THF (TH1)

• Constants for binders
• Types ... TH0 + TF1
• Type signatures ... TH0 + TF1
• Some types provided for uses of polymorphic symbols
• ATP systems ... HOLyHammer, Leo-III, Vampire, Zipperposition, etc.
• Example (as a plain file)

  thf(dog_type,type,      dog: $tType ).         thf(human_type,type,    human: $tType ).
  thf(biter_type,type,    biter: $tType > $tType ).
  thf(odie_decl,type,     odie: (biter @ dog) ). thf(jon_decl,type,      jon: human ).
  
  thf(owner_of_decl,type, owner_of:
      !>[BiterType: $tType] : ( ( biter @ BiterType ) > human ) ).
  thf(owns_decl,type,     owns:
      !>[BiterType: $tType] : ( human > ( biter @ BiterType ) > $o ) ).
  thf(bit_decl,type,      bit:
      !>[BiterType: $tType] : ( ( biter @ BiterType ) > human > $int > $o ) ).
  thf(hates_decl,type,    hates: human > human > $o ).
  thf(feeds_decl,type,    feeds: human > (biter @ dog) > $o ).
  thf(chases_decl,type,   chases: human > (biter @ dog) > $o ).
  thf(says_decl,type,     says: human > $o > $o ).
  
  thf(owns_defn,definition,
      ( owns
      = ( ^ [T: $tType,H: human,B: biter @ T] : ( H = ( owner_of @ T @ B ) ) ) ) ).
  
  thf(jon_owns_odie,axiom,                       thf(odie_bit_jon_twice,axiom,
      owns @ dog @ jon @ odie ).                     bit @ dog @ odie @ jon @ 2 ).
  
  thf(hate_the_multi_biter_any,axiom,            thf(feed_the_non_biter_dog,axiom,
      ! [T: $tType,B: biter @ T,                     ! [D: biter @ dog,H: human] :
                   H: human,N: $int] :                 $ite(
        ( ( ~ ( owns @ T @ H @ B )                       ? [N: $int] :
          & ( bit @ T @ B @ H @ N )                        ( ( bit @ dog @ D @ H @ N )
          & ( $greater @ N @ 1 ) )                         & ( $greater @ N @ 0 ) ),
       => ( hates @ H @ ( owner_of @ T @ B ) ) ) ).      chases @ H @ D,
                                                         feeds @ H @ D) ).
  thf(jon_says_a_dog_bit_him_twice,axiom,
      ? [D: biter @ dog] :                       thf(jon_says_truth,axiom,
        ( ( D != odie )                              ! [S: $o] :
        & ~ ( owns @ dog @ jon @ D )                   ( ( says @ jon @ S )
        & ( says @ jon @                              => S ) ).
            ( bit @ dog @ D @ jon @ 2 ) ) ) ).
  
  thf(jon_chases_and_feels,conjecture,
      ? [D: biter @ dog,H: human,F: human > human > $o] :
        ( ( chases @ jon @ D )
        & ( H != jon )
        & ( F @ jon @ H ) ) ).