# Non-classical Typed Logic (NTF)

### Alethic Mono-Modal Logic T Problem

• Axioms
• If there is a product that a person works hard on, then it's possible 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:persongets_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 ==
[ \$constants == \$rigid,
\$quantification == \$constant,
\$modalities == \$modal_system_T ] ).

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 it in SystemOnTPTP using Leo-III.

### 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 T.

### Epistemic Multi-Modal Logic S4 Problem

• Axioms
• The bank knows that, for all account numbers, the conversational record knows that if Geoff has an account with a given number then there is an amount that the teller knows is Geoff's balance.
• The conversational record knows that 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:amountteller A = balance_of(geoff)

### In TPTP format

• ```tff(s4_constant_rigid,logic,
\$epistemic_modal ==
[ \$constants == \$rigid,
\$quantification == \$constant,
\$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

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.