Non-classical Typed Logic (NTF)

New logic features

• Modal connectives {connective}
  can be indexed for multi-modal forms {connective(#index)}
• See the table of non-classical logics in the TPTP World
• Logic specifications.
• For modal logics, see the modal logic cube
• Non-classical eXtended First-order (NXF) and Higher-order (NHF)
• The examples are in monomorphic NXF (NX0)

Alethic Mono-Modal Logic M Problem

• Axioms
  • If there is a product that a person works hard on, then it's possible that the person will get rich.
  • Nobody necessarily gets rich.
  • Alex and Chris work hard on Leo-III.
• Conjecture
  • It's possible that Alex gets rich but it's also possible that Chris does not.

In logic

• Type information
  • person is a type.
  • product is a type.
  • Alex and Chris are persons
  • Leo is a product
  • works_hard takes a person and a product argument, and returns a boolean.
  • gets_rich takes a person argument, and returns a boolean.
• Axioms
  • ∀ P:person ( ∃ R:product works_hard(P,R) → ◊ gets_rich(P))
  • ¬ ∃ P:person □ gets_rich(P)
  • works_hard(alex,leo) ∧ works_hard(chris,leo)
• Conjecture
  • ◊ gets_rich(alex) ∧ ◊ ¬ gets_rich(chris)

In TPTP format

• tff(semantics,logic,
      $alethic_modal ==
        [ $domains == $constant,
          $designation == $rigid,
          $terms == $local,
          $modalities == $modal_system_M ] ).
  
  tff(person_decl,type,person: $tType).
  tff(product_decl,type,product: $tType).
  tff(alex_decl,type,alex: person).
  tff(chris_decl,type,chris: person).
  tff(leo_decl,type,leo: product).
  tff(work_hard_decl,type,work_hard: (person * product) > $o).
  tff(gets_rich_decl,type,gets_rich: person > $o).
  
  tff(work_hard_to_get_rich,axiom,
      ! [P: person] :
        ( ? [R: product] : work_hard(P,R) => ( {$possible} @ (gets_rich(P)) ) ) ).
  
  tff(not_all_get_rich,axiom,
      ~ ? [P: person] : ( {$necessary} @ (gets_rich(P)) ) ).
  
  tff(alex_works_on_leo,axiom,
      work_hard(alex,leo) ).
  
  tff(chris_works_on_leo,axiom,
      work_hard(chris,leo) ).
  
  tff(only_alex_gets_rich,conjecture,
      ( ( {$possible} @ (gets_rich(alex)) ) & ( {$possible} @ (~ gets_rich(chris)) ) ) ).
  

• Check the syntax in SystemB4TPTP using BNFParser.
• Try prove it using Leo-III in SystemOnTPTP.

Challenge problem

Epistemic Multi-Modal Logic S4 Problem

• Axioms
  • The bank knows that if Geoff has an account with a given number then Geoff has some amount of money (in the account)
  • Geoff's account number is 42
• Conjecture
  • There is an amount that the teller can know is Geoff's balance

In logic

• Type information
  • customer is a type
  • amount is a type
  • Account numbers are integers
  • geoff is a customer
  • account takes a customer and an acount number and returns a boolean
  • balance_of takes a customer and returns an amount.
• Axioms
  • □_bank (∃ N:integer account(geoff,N) → ∃ A:amount A = balance_of(geoff))
  • account(geoff,42)
• Conjecture
  ∃ A:amount ◊_teller A = balance_of(geoff)

In TPTP format

• tff(semantics,logic,
      $epistemic_modal ==
        [ $domains == $constant,
          $designation == $rigid,
          $terms == $local,
          $modalities == $modal_system_S4 ] ).
  
  tff(customer_decl,type,customer: $tType).
  tff(amount_decl,type,amount: $tType).
  tff(geoff_decl,type,geoff: customer).
  tff(account_decl,type,account: (customer * $int) > $o).
  tff(balance_decl,type,balance_of: customer > amount).
  
  tff(bank_knows_accounts,axiom,
      {$knows(#bank)} @
        ( ? [N: $int] : account(geoff,N)
       => ? [A: amount] : A = balance_of(geoff) ) ).
  
  tff(geoffs_account_42,axiom,
      account(geoff,42) ).
  
  tff(teller_can_know_balance,conjecture,
      ? [A: amount]: {$canKnow(#teller)} @ (A = balance_of(geoff)) ).
  

• Check the syntax in SystemB4TPTP using BNFParser.
• Try it in SystemOnTPTP using Leo-III.

Challenge problem