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:human ∀ H2: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