Typed 1st Order Logic

Typed first-order logic (also called many sorted logic) extends untyped first-order logic by adding a finite number of distinct types. Predicates and functors are declared with type signatures than specify the types of the arguments and the return type, and variables are given types in their quantification.

The Language of Typed 1st order logic

A typed 1st order language consists of four sets of symbols: TPTP syntax is used here: variables start with upper case alphbetic, and functors, predicate, and type symbols start with lower case alphabetic. When referring directly to a functor or predicate symbol, its arity is given after a , e.g., in blah/2, blah is the functor or predicate symbol and the arity is 2. TPTP Typed First-order Form (TFF) formulae are written in tff(...) annotated formulae. The TPTP world predefines several types: User types are declared to be of the psuedo-type $tType. All user types, and the type signatures of constants, functors, and predicates, should be declared before use, in annotated formulae with the role type (those that are not declared get default type signatures using $i and $o). The types of variables are declared in their quantification. Equality is adhoc polymorphic over the types, requiring that both arguments have the same type.
Example 
tff(cat_type,type, cat: $tType ).
tff(dog_type,type, dog: $tType ).
tff(human_type,type, human: $tType ).

tff(garfield_decl,type, garfield: cat ).
tff(odie_decl,type, odie: dog ).
tff(jon_decl,type, jon: human ).
tff(owner_of_cat_decl,type, owner_of_cat: cat > human ).
tff(owner_of_dog_decl,type, owner_of_dog: dog > human ).
tff(chased_decl,type, chased: ( dog * cat ) > $o ).
tff(hates_decl,type, hates: ( human * human ) > $o ).

tff(jon_owns_garfield,axiom,
    jon = owner_of_cat(garfield) ).

tff(jon_owns_odie,axiom,
    jon = owner_of_dog(odie) ).

tff(jon_owns_only_cat,axiom,
    ! [C: cat] :
      ( ( jon = owner_of_cat(C) )
     => ( C = garfield ) ) ).

tff(jon_owns_only_dog,axiom,
    ! [D: dog] :
      ( ( jon = owner_of_dog(D) )
     => ( D = odie ) ) ).

tff(dog_chase_cat,axiom,
    ! [D: dog,C: cat] :
      ( chased(D,C)
     => hates(owner_of_cat(C),owner_of_dog(D)) ) ).

Subtypes are not available (yet), so this is not allowed ... 

    tff(pet_type,type, pet: $tType ).
    tff(cat_type,type, cat: $tType ).
    tff(dog_type,type, dog: $tType ).
    tff(cat_pet_type,type, ( cat << pet ) ).
    tff(dog_pet_type,type, ( dog << pet ) ).
    tff(human_type,type, human: $tType ).
    
    tff(garfield_decl,type, garfield: cat ).
    tff(odie_decl,type,odie: dog ).
    tff(jon_decl,type, jon: human ).
    tff(owner_of_decl,type, owner_of: pet > human ).
    tff(chased_decl,type, chased: ( dog * cat ) > $o ).
    tff(hates_decl,type, hates: ( human * human ) > $o ).
    
    tff(jon_owns_garfield,axiom, jon = owner_of(garfield) ).
    tff(jon_owns_odie,axiom, jon = owner_of(odie) ).
    tff(jon_owns_only_cat,axiom,
        ! [P: pet] :
          ( ( jon = owner_of(P) )
         => ( ( P = garfield ) | ( P = odie ) ) ) ).
    tff(dog_chase_cat,axiom,
        ! [D: dog,C: cat] :
          ( chased(D,C)
         => hates(owner_of(C),owner_of(D)) ) ).
One way to solve this is to use a type-promotion function ...
Example 
tff(cat_to_pet_decl,type, cat_to_pet: cat > pet ).
tff(dog_to_pet_decl,type, dog_to_pet: dog > pet ).

tff(jon_owns_garfield,axiom,
    jon = owner_of(cat_to_pet(garfield)) ).

tff(jon_owns_odie,axiom,
    jon = owner_of(dog_to_pet(odie)) ).

tff(jon_owns_only,axiom,
    ! [P: pet] :
      ( ( jon = owner_of(P) )
     => ( ( P = cat_to_pet(garfield) )
        | ( P = dog_to_pet(odie) ) ) ) ).

tff(dog_chase_cat,axiom,
    ! [D: dog,C: cat] :
      ( chased(D,C)
     => hates(owner_of(cat_to_pet(C)),owner_of(dog_to_pet(D))) ) ).

Translation from English to Typed 1st Order Logic

There is often a direct translation from a problem stated in a natural language to typed 1st order logic.

Example
Every student is enrolled in at least one course. Every professor teaches at least one course. Every course has at least one student enrolled. Every course has at least one professor teaching it. The coodinator of a course is a professor who is teaching it. If a student is enrolled in a course then the student is taught by every professor who teaches the course. CSC410 is a course. Michael is a student enrolled in CSC410. Victor is the coordinator of CSC410. Therefore, Michael is taught by Victor. 
T = { student, professor, course }
V = { V : V starts with uppercase }
F = { michael/0, victor/0, csc410/0, coordinator_of/1 }
P = { student/1, professor/1, course/1, enrolled/2, teaches/2, taught_by/2 }


tff(student_type,type, student: $tType ).
tff(professor_type,type, professor: $tType ).
tff(course_type,type, course: $tType ).

tff(michael_decl,type, michael: student ).
tff(victor_decl,type, victor: professor ).
tff(csc410_decl,type, csc410: course ).
tff(coordinator_of_decl,type, coordinator_of: course > professor ).
tff(enrolled_decl,type, enrolled: ( student * course ) > $o ).
tff(teaches_decl,type, teaches: ( professor * course ) > $o ).
tff(taught_by_decl,type, taught_by: ( student * professor ) > $o ).

%----Every student is enrolled in at least one course.
tff(each_enrolled,axiom,
    ! [S: student] :
    ? [C: course] : enrolled(S,C) ).

%----Every professor teaches at least one course.
tff(each_teaches,axiom,
    ! [P: professor] :
    ? [C: course] : teaches(P,C) ).

%----Every course has at least one student enrolled.
tff(course_students,axiom,
    ! [C: course] :
    ? [S: student] : enrolled(S,C) ).

%----Every course has at least one professor teaching it.
tff(course_professors,axiom,
    ! [C: course] :
    ? [P: professor] : teaches(P,C) ).

%----The coodinator of a course is a professor who is teaching it.
tff(course_coordinator,axiom,
    ! [C: course] : teaches(coordinator_of(C),C) ).

%----If a student is enrolled in a course then the student is taught by every
%----professor who teaches the course.
tff(enrolled_taught,axiom,
    ! [S: student,C: course] :
      ( enrolled(S,C)
     => ! [P: professor] :
          ( teaches(P,C)
         => taught_by(S,P) ) ) ).

%----CSC410 is a course. In the type declarations

%----Michael is a student enrolled in CSC410.
tff(michael_csc410,axiom,
    enrolled(michael,csc410) ).

%----Victor is the coordinator of CSC410.
tff(victor_csc410,axiom,
    coordinator_of(csc410) = victor ).

%----Therefore, Michael is taught by Victor.
tff(michael_victor,conjecture,
    taught_by(michael,victor) ).

Educational Example

Exercises

Convert the following into typed 1st order logic:

Interpretation

Interpretation of typed 1st order formulae requires a slightly more complex structure than for first-order logic.

An interpretation of a typed 1st order logic consists of three parts:

Conversion to Untyped 1st Order Logic

Types first-order logic can be translated to untyped first-order logic. Each type becomes a new unary predicate in the untyped world.

Exam Style Questions