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
- grade_of takes one human argument and returns their grade
- created_equal takes two human arguments and returns boolean
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_decl,type,human: $tType).
tff(grade_decl,type,grade: $tType).
tff(john_decl,type,john: human).
tff(a_decl,type,a: grade).
tff(f_decl,type,f: grade).
tff(grade_of_decl,type,grade_of: human > grade).
tff(created_equal_decl,type,created_equal: (human * human) > $o).

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.
Check the axioms are consistent with Vampire-SAT in SystemOnTPTP.
Try prove it using Vampire in SystemOnTPTP.
View the derivation using IDV in SystemOnTSTP.
Verify the derivation using GDV in SystemOnTSTP.

Challenge problem

Geoff is the only 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 than Joe, also taught by Geoff, who also failed.

Non-theorems

Axioms
- Jon is the only human.
- Garfield, Arlene, and Nermal are the only (distinct) cats.
- Jon owns Garfield, but does not own Arlene.
- The cat that all cats love is Garfield.
Conjecture
- Jon owns all cats that love Garfield, except for Arlene.

In TPTP format

tff(human_type,type,      human: $tType ).
tff(cat_type,type,        cat: $tType ).
tff(jon_decl,type,        jon: human ).
tff(garfield_decl,type,   garfield: cat ).
tff(arlene_decl,type,     arlene: cat ).
tff(nermal_decl,type,     nermal: cat ).
tff(loves_decl,type,      loves: cat > cat ).
tff(owns_decl,type,       owns: ( human * cat ) > $o ).

tff(only_jon,axiom, ! [H: human] : H = jon ).

tff(only_garfield_and_arlene_and_nermal,axiom,
    ! [C: cat] :
      ( C = garfield | C = arlene | C = nermal ) ).

tff(distinct_cats,axiom,
    ( garfield != arlene & arlene != nermal
    & nermal != garfield ) ).

tff(jon_owns_garfield_not_arlene,axiom,
    ( owns(jon,garfield) & ~ owns(jon,arlene) ) ).

tff(all_cats_love_garfield,axiom,
    ! [C: cat] : ( loves(C) = garfield ) ).

tff(jon_owns_garfields_lovers,conjecture,
    ! [C: cat] :
      ( ( loves(C) = garfield & C != arlene )
     => owns(jon,C) ) ).

Check the syntax using TPTP4X in SystemB4TPTP.
Check the axioms are consistent with Vampire-SAT in SystemOnTPTP.
Try prove it using Vampire in SystemOnTPTP.
Disprove it using Vampire-FMo SystemOnTPTP. That produces a (non-TPTP-compliant) finite countermodel. Here's a counter model in the new TPTP format.
View the finite countermodel using IIV in SystemOnTSTP.
Verify the finite countermodel using AGMV in SystemOnTSTP. Use the concatenation of the problem and the countermodel as input.