# Typed First-order Logic (TFF)

### New logic features

• Types
• Signatures
• Typed variables

### Problem

• Axioms
• All (hu)men are created equal.
• John is a human.
• John got an F grade.
• There is some human who got an A grade.
• An A grade is not equal to an F grade.
• Conjecture
• There is a human other than John, who was created equal to John

### In logic

• Type information
• human is a type
• grade is a type
• john is a human
• a is a grade
• f is a grade
• created_equal takes two human arguments and returns boolean
• grade_of takes one human argument and returns their grade
• Axioms
• H1:humanH2:human created_equal(H1,H2)
• grade_of(john) = f
• H:human grade_of(H) = a
• a ≠ f
• Conjecture
• H:human (H ≠ john ∧ created_equal(H,john))

### In TPTP format

• ```tff(human_type,type,human: \$tType).
tff(grade_type,type,grade: \$tType).
tff(john_type,type,john: human).
tff(a_type,type,a: grade).
tff(f_type,type,f: grade).
tff(created_equal_type,type,created_equal: (human * human) > \$o).
tff(grade_of_type,type,grade_of: human > grade).

tff(all_created_equal,axiom,
! [H1:human,H2:human] : created_equal(H1,H2) ).
tff(john_got_an_f,axiom,
grade_of(john) = f ).
tff(someone_got_an_a,axiom,
? [H:human] : grade_of(H) = a ).
tff(a_is_not_f,axiom,
a != f ).

tff(there_is_someone_else,conjecture,
? [H:human] :
( H != john
& created_equal(H,john) ) ).
```
• Check the syntax in SystemB4TPTP using TPTP4X.
• Try it in SystemOnTPTP using Vampire.

### Challenge problem

Geoff is the teacher of Joe. Joe is not stupid but Joe failed. If a student failed then either the student is stupid or there is is some other student with the same teacher who also failed. Therefore there is some student other then Joe and also taught by Geoff, who failed. Optional: Assume that each student has only one teacher, so that, e.g., Geoff is the only teacher of Joe and the other student.