# Typed Higher-order Logic (THF)

### New logic features

• Functions and predicates conflated
• Variable functions and predicates
• Lambda functions with λ (lambda)
• Partial application

### Problem

• Axioms
• Coffee is a beverage.
• A heated beverage is a beverage.
• A mixture of a beverage with a syrup is a beverage.
• A heated mix is the application of heat to the mixture of a beverage with a syrup.
• A heated mixture is hot!
• A heated mixture of coffee and any syrup is still coffee.
• Conjecture
• There is something that when mixed with any syrup results in hot coffee.

### In logic

• Type information
• beverage is a type
• syrup is a type
• coffee is a beverage
• mix takes a beverage and a syrup argument and returns a beverage
• heat takes a beverage argument and returns a beverage
• heated_mix takes a beverage and a syrup argument and returns a beverage
• hot takes a beverage argument and returns boolean
• Axioms
• heated_mix = λ B:beverage,S:syrup (heat (mix B S))
• B:beverageS:syrup (hot (heated_mix B S))
• S:syrup (heated_mix coffee S) = coffee
• Conjecture
• M:syrup > beverageS:syrup (M S) = coffee ∧ (hot (M S))

### In TPTP format

• ```%------------------------------------------------------------------------------
thf(beverage_type,type,beverage: \$tType).
thf(syrup_type,type,syrup: \$tType).
thf(coffee_type,type,coffee: beverage).
thf(mix_type,type,mix: beverage > syrup > beverage).
thf(heat_type,type,heat: beverage > beverage ).
thf(heated_mix_type,type,heated_mix: beverage > syrup > beverage).
thf(hot_type,type,hot: beverage > \$o).

thf(heated_mix,axiom,
heated_mix = ( ^ [B: beverage,S :syrup] : ( heat @ ( mix @ B @ S ))) ).

thf(hot_mixture,axiom,
! [B: beverage,S: syrup] : ( hot @ ( heated_mix @ B @ S ) ) ).

thf(heated_coffee_mix,axiom,
! [S: syrup] : ( ( heated_mix @ coffee @ S ) = coffee ) ).

thf(hot_coffee,conjecture,
? [Mixture: syrup > beverage] :
! [S: syrup] :
( ( ( Mixture @ S ) = coffee )
& ( hot @ ( Mixture @ S ) ) ) ).
%------------------------------------------------------------------------------
```
Note how the signatures of symbols whose arity is greater than 1 are provided in curried form, which allows for partial application.
• Check the syntax in SystemB4TPTP using TPTP4X.
• Try it in SystemOnTPTP using Leo-III.

### Challenge problem

Andrew, Betty, and Charlie are (different) people. Andrew loves himself, Betty does not love herself. Selfish love is a relationship between two (different) people in which the second person loves themself (and the first person is ignored). Prove that there exists a property of a person that is true for Andrew but not for Betty.