The NXF and NHF Languages

Within the TXF and THF Languages

Connectives

• Long form, e.g., {$necessary}, {$possible}.

  tff(no_flying_pigs,axiom,(
      ~ ( {$possible} @ (pigs_might_fly) ) )).
  
  thf(flying_pigs,axiom,(
      {$necessary} @ pigs_might_fly )).  

• Short form, e.g., [.], <.>

  tff(flying_pigs,axiom,(
      [.](pigs_might_fly) )).
  
  thf(no_flying_pigs,axiom,(
      ~ ( <.> @ pigs_might_fly ) )).  

• Indexed, e.g., {$necessary:#index}, <#index>

  tff(for_me_it_is_possible,axiom,(
      {$possible(#me)} @ (pigs_might_fly) )).
  
  thf(for_me_somthing_is_possible,axiom,(
      ? [P: $o] : ( {$possible(#me)} @ P ) )).  

• Parameterised, e.g., $common:$group:=[group members]

  tff(common_knowledge,axiom,(
      {$common($group:=[jane,albert,mary])} @ (something_known_by_all_three) )).  

Kripke Worlds

• By default, axioms hold in all worlds
• By default, hypothesiss hold in the current world
• By default, conjectures are proved in the current world
• Subroles -local or -global override the defaults

  tff(for_me_here_it_is_possible,axiom-local,(
      {$possible(#me)} @ (pigs_might_fly) )).
  
  thf(somthing_is_always_possible,conjecture-global,(
      ? [P: $o] : ( {$possible} @ P ) )).  

Logic Specifications

• Specify the semantic framework to be used for reasoning
• For logics interpreted using Kripke semantics
  • Rigid or flexible constants
  • Constant, varying, cumulative, or decreasing domains
  • Local or global extension
  • Modal system (by name, or maybe by axioms)
• Simple S5

  tff(simple_s5,logic,(
      $modal ==
        [ $rigidity == $rigid,
          $domains == $constant,
          $locality == $local,
          $modalities == $modal_system_S5 ] )).  

• With defaults

  thf(with_defaults,logic,(
      $modal ==
        [ $rigidity == $rigid,
          $domains ==
            [ $constant,
              plushie == $varying ],
          $locality == $local,
          $modalities == 
            [ $modal_system_S4,
              #king_of_france == $modal_system_S5 ] ] )).  

Examples

• Work to get Rich
• Bank Tellers Know