Non-classical Typed Forms

Non-classical Typed Forms (NTF)

• Hot off the press!
• First-order (NXF) based on TXF, higher-order (NHF) based on THF
• Monomorphic (NX0, NH0) and polymorphic (NX1, NH1)
• Semantics of non-classical polymorphic unclear
• Logic specifications, non-classical connectives

Logic specifications

• Specify logic to be used, with properties
• Example

     tff(simple_spec,logic,
         $modal == [
           $constants == $rigid,
           $quantification == [ $constant, some_user_type == $varying ],
           $modalities == $modal_system_S5 ] ).
  

• By default axioms are global, hypothesises are local, conjectures are local; can override.

Non-classical Connectives

• {$connective_name(parameters)}
• parameters ... #index, key:=value
• ATP systems ... Leo-III, that's all folks (right now)
• NX0 Example (as a plain file)

  tff(garfield,logic,
      $modal == [
        $constants == $rigid,
        $quantification == $constant,
        $modalities == $modal_system_S5 ] ).
  
  tff(dog_decl,type,      dog: $tType ).      tff(human_decl,type,    human: $tType ).
  tff(odie_decl,type,     odie: dog ).        tff(jon_decl,type,      jon: human ).
  tff(owner_of_decl,type, owner_of: dog > human ).
  tff(bit_decl,type,      bit: (dog * human * $int) > $o ).
  tff(hates_decl,type,    hates: (human * human) > $o ).
  tff(feeds_decl,type,    feeds: (human * dog) > $o ).
  tff(chases_decl,type,   chases: (human * dog) > $o ).
  tff(says_decl,type,     says: (human * $o) > $o ).
  
  tff(jon_owns_odie,axiom,                    tff(odie_bit_jon_twice,axiom,
      jon = owner_of(odie) ).                     bit(odie,jon,2) ).
  
  tff(hate_the_multi_biter_dog,axiom,         tff(feed_the_non_biter_dog,axiom,
      ! [D: dog,H: human,N: $int] :               ! [D: dog,H: human] :
        ( ( H != owner_of(D)                        $ite(
          & bit(D,H,N)                                ? [N: $int] :
          & $greater(N,1) )                             ( bit(D,H,N)
       => {$necessary(#arlene)} @                       & $greater(N,0) ),
            hates(H,owner_of(D)) ) ).                 chases(H,D),
                                                      feeds(H,D)) ).
  
  tff(jon_says_a_dog_bit_him_twice,axiom,     tff(jon_says_truth,axiom,
      ? [D: dog] :                                ! [S: $o] :
        ( D != odie                                 ( says(jon,S)
        & jon != owner_of(D)                       => S ) ).
        & says(jon,bit(D,jon,2)) ) ).
  
  tff(jon_chases_and_hates,conjecture,
      ? [D: dog,H: human] :
        ( {$possible(#garfield)} @ chases(jon,D)
        & H != jon
        & hates(jon,H) ) ).
  
  

• NX1 Example (as a plain file)
• NH0 Example (as a plain file)

  thf(semantics,logic,(
    $modal ==
      [ $constants == $rigid,
        $quantification == $constant,
        $modalities == $modal_system_S5 ] )).
  
  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-local,               thf(odie_bit_jon_twice,axiom-local,
       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 )
       => ( {$necessary(#arlene)} @                    & ( $greater @ N @ 0 ) ),
            ( hates @ H @                              chases @ H @ D,
              ( owner_of @ D ) ) ) ) ).                feeds @ H @ D) ).
  
  thf(jon_says_a_dog_bit_twice,axiom-local,    thf(jon_says_truth,axiom,
      ? [D: dog] :                                 ! [S: $o] :
        ( ( D != odie )                              ( ( says @ jon @ S )
        & (~ ( owns @ jon @ D ))                    => S ) ).
        & ( says @ jon @ (
            bit @ D @ jon @ 2 ) ) ) ).
  
  thf(jon_chases_and_feels,conjecture,
      ? [D:dog,H: human,F: human > human > $o] :
        ( ( {$possible(#garfield)} @ ( chases @ jon @ D ) )
        & ( H != jon )
        & ( F @ jon @ H ) ) ).
  

• NH1 Example (as a plain file)