Non-classical Typed Logic (NTF)

New logic features

Many different logics
Modal connectives necessary/obligatory/knows/etc. and possible/permissible/believes/etc.
Modal connectives can be indexed, for multi-modal logic
Kripke semantics

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.

Challenge problem

Every student thinks that it's possible that some exam is unfair towards them. If some student is cheating on an exam, then the exam is necessarily unfair to every student. Donald is cheating on the CSC101 exam. Therefore it's possible that there's an exam that is unfair to Alex. Use alethic mono-modal logic M.

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

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 using TPTP4X in SystemB4TPTP.
Try prove it using Leo-III in SystemOnTPTP.

Challenge problem

For all logics, Geoff knows they are complicated. Prove that Geoff can know that Alex knows that Geoff knows that modal logic is complicated. Use epistemic multi-modal logic S4.