The Type System

A high-level overview is in the section on annotated formulae.

Subtypes
None of the type systems offer subtypes, despite the subtype symbol << being part of the THF and TFF languages. I tried to convince the ATP system developers it would be useful, but they cried crocodile tears. Here's an example of what was planned: 

    tff(food_type,type, food: $tType).

    tff(fruit_type,type, fruit: $tType).

    tff(vegetable_type,type, vegetable: $tType).

    tff(fruit_is_food,type, 
        fruit << food ).

    tff(vegetable_is_food,type, 
        vegetable << food ). 

    tff(apple_decl,type, apple: fruit).

    tff(potatoe_decl,type, potatoe: vegetable).
All subtypes of an atomic type are disjoint, i.e., it is implicit that apple != potatoe.

The Typed First-order Monomorphic Type System (TF0 and TX0)

Refer to [SS+12] (TF0) and [SK18] (TX0) for more details on type checking and semantics, and much more.

Defined atomic types
The atomic types $i (individuals), $o (Booleans), and $tType are defined. ($tType is the "type" of atomic types - it is not really a type, and in other places this is known as the "kind" of atomic types. See below for motivation for its existence and usage.) Other defined atomic types are associated with specific theories. In particular, $int, $rat, and $real are types for arithmetic. The type $i of individuals is predefined but has no peculiar semantics, whereas the arithmetic types $int, $rat, and $real are modeled by ℤ, ℚ, and ℝ, respectively.

User atomic type declarations:
User atomic types are declared in advance of use, to be of "type" $tType. Example: 

    tff(food_type,type, 
        food: $tType ).

    tff(fruit_type,type, 
        fruit: $tType ).

    tff(list_type,type, 
        list: $tType ).

Defined functions and predicates
Defined functions and predicates have preassigned types.

Function and predicate type declarations
Every function and predicate symbol has maximally one declared type. Example: 

    tff(cons_type,type, 
        cons: (fruit * list) > list   ).

    tff(is_empty_type,type, 
        isEmpty: list > $o   ).
The argument types must be atomic, and cannot be $o in TFF, but can be $o in TXF. The range type of a function must be atomic, and cannot be $o. The range type of a predicate is $o. Currying is not possible in TFF or TXF, i.e., the first example above cannot be written cons: fruit > list > list (currying is used in THF and DHF). If a symbol's type is declared more than once, and the types are not the same, that's an error.

Every variable is given an atomic type at quantification time. Example: 

    tff(list_not_empty,axiom, 
        ! [X: fruit,Xs: list] : ~isEmpty(cons(X,Xs))   ).

Implicit typing for functions and predicates
If a symbol is used and its type has not been declared, then default types are assumed.

If a symbol's type is declared later to be different from the assumed type, that's an error.

The Typed First-order Polymorphic Type System (TF1 and TX1)

Refer to [BP13] for more details on type checking and semantics, and much more.

The TF1 polymorphic type system extends the monomorphic type system with rank-1 polymorphism. Syntactically, the types, terms, and formulas of TF1 are analogous to those of TF0, except that function and predicate symbols can be declared to be polymorphic, types can contain type variables, and n-ary type constructors are allowed. Type variables in type signatures and formulas are explicitly bound. Instances of polymorphic symbols are specified by explicit type arguments, rather than inferred.

Types and type signatures
The types of TF1 are built from type variables and type constructors of fixed arities. A type is polymorphic if it contains type variables (otherwise, it is monomorphic). Polymorphic type signatures are of the form: !>[α1 : $tType, ..., αn : $tType]: ς for n > 0, where α1, ..., αn are distinct type variables and ς is a monomorphic type. The binder !> denotes universal quantification.

Type declarations
Type constructors can be declared, e.g., the following declarations introduce a type constant bird, a unary type constructor list, and a binary type constructor map: 

    tff(bird_t, type, bird: $tType).
    tff(list_t, type, list: $tType > $tType).
    tff(map_t, type, map: ($tType * $tType) > $tType).
Every type variable must be bound by a !>-binder. The following declarations introduce a polymorphic predicate is_empty, and a pair of polymorphic functions cons and lookup: 
    tff(is_empty_t, type, is_empty : !>[A : $tType]: (list(A) > $o)).
    tff(cons_t, type, cons : !>[A : $tType]: ((A * list(A)) > list(A))).
    tff(lookup_t, type, lookup : !>[A : $tType, B : $tType]: ((map(A, B) * A) > B)).

Using symbols with a polymorphic type
Every use of a polymorphic symbol must explicitly specify the type instance. A function or predicate symbol with a type signature !>[α1$: $tType, ..., αm : $tType]: ((τ1 * ... * τn) > υ) must be applied to m type arguments and n term arguments. Given the above signatures, the term lookup($int, list(A), M, 2) and the atom is_empty($i, cons($i, X, nil($i))) are well-formed and contain free occurrences of the type variable A and the term variable X, respectively. As TF1 is restricted to rank-1 polymorphism, type variables can be instantiated with only concrete types. In particular, $o, $tType, and !>-binders cannot occur in type arguments of polymorphic symbols.

Every variable in a TF1 formula must be bound. In particular, every type variable in a TF1 formula must be bound with the pseudotype $tType: 

    tff(bird_list_not_empty, axiom,
        ![B : bird, Bs : list(bird)]: ~ is_empty(bird, cons(bird, B, Bs))).

    tff(lookup_update_same, axiom,
        ! [A : $tType, B : $tType, M : map(A, B), K : A, V : B]:
          lookup(A, B, update(A, B, M, K, V), K) = V).
Universal and existential quantifiers over type variables may not occur in the scope of a quantifier over a term variable (as is possible in dependent types).

Example
An example TF1 problem is PUZ139_1.

The Typed Higher-order Monomorphic Type System (TH0)

Refer to [SB10] for more details on type checking and semantics, and much more.

The TH0 monomorphic type system lifts the TF0 type system to simply typed λ-calculus, with Henkin semantics (i.e., including Boolean and functional extensionality) and choice. Type signatures are curried, and variables can have function types. Example: 

    thf(mix_type,type,
        mix: beverage > syrup > beverage ).
    
    thf(mixed_coffee,conjecture,
        ? [Mixture: beverage > syrup > beverage] :
        ! [S: syrup] :
          ( ( Mixture @ coffee @ S ) = coffee ) ).

An example TH0 problem is PUZ140^1.

The Typed Higher-order Polymorphic Type System (TH1)

Refer to [KSR16] for more details on type checking and semantics, and much more.

The TH1 polymorphic type system combines the polymorphic features of TF1/TX1 with the higher-order features of TH0.
Example: 

    thf(list,type, list: $tType > $tType ).
    
    thf(nil,type, nil: !>[A: $tType] : ( list @ A ) ).
    
    thf(append,type, append: !>[A: $tType] : ( ( list @ A ) > ( list @ A ) > ( list @ A ) ) ).
    
    thf(append_nil,axiom,
        ! [A: $tType,L: list @ A] :
          ( ( append @ A @ ( nil @ A ) @ L ) = L ) ).

TH1 has five additional polymorphic constants: !! for Π (universal quantification), ?? for Σ (existential quantification), @@+ for ε (indefinite description, aka choice), @@- for ι (definite description), and @= (equality). The type of the first four is !>[A: $tType] : (A > $o) > $o, and the type of @= is !>[A: $tType]: (A > A) > $o. When used they must be instantiated by applying them to a type argument. Example: 

    thf(eps,type, eps: ( $i > $o ) > $i ).
    
    thf(choiceax,axiom,
        ! [P: $i > $o] :
          ( ? [X: $i] : ( P @ X )
         => ( P @ ( eps @ P ) ) ) ).
    
    thf(conj,conjecture,
        ( ( ^ [P: $i > $o] : ( P @ ( eps @ P ) ) )
        = ( ^ [P: $i > $o] : ( ?? @ $i @ P ) ) ) ).
    
    thf(bird_type,type, bird: $tType).

    thf(tweety_decl,type, tweety: bird).

    thf(some_tweety,axiom,
        ? [B: bird] : ( (@= @ bird) @ tweety @ B ) ).

An example TH1 problem is DAT434^1.

The Dependently Typed Higher-order Type System (DH0 and DH1)

Refer to [RK+25] for more details on type checking and semantics, and much more.

The DH0 and DH1 type systems add dependent types, i.e., types that take term arguments, to TH0 and TH1. As such they are classical and extensional type theories. The !> binder used for TF1 and TH1 polymorphism is reused to specify the term typess on which a type depends. Example: 

    thf(elem_type,type, elem: $tType ).

    thf(nat_type,type, nat: $tType ).

    thf(zero_type,type, zero: nat ).

    thf(suc_type,type, suc: nat > nat ).

    thf(plus_type,type, plus: nat > nat > nat ).

    thf(list_type,type, list: nat > $tType ).

    thf(nil_type,type, nil: list @ zero ).

    thf(cons_type,type, cons:
        !>[N: nat] : (elem > (list @ N) > (list @ (suc @ N))) ).

    thf(app_type,type, app:
        !>[N: nat,M: nat] : ((list @ N) > (list @ M) > (list @ (plus @ N @ M))) ).
The application operator @ is used to instantiate the terms to the dependent type. With polymorphic types, the variable list is prepended with the type variables. Example: 
    thf(ax1,axiom,
        ! [N: nat] : ((plus @ zero @ N) = N) ).

    thf(ax2,axiom,
        ! [N: nat,X: list @ N] : ((app @ zero @ N @ nil @ X) = X) ).

    thf(list_app_assoc_base,conjecture,
        ! [M2: nat,L2: list @ M2,M3: nat,L3: list @ M3] :
          ( ( app @ zero @ ( plus @ M2 @ M3 ) @ nil @ ( app @ M2 @ M3 @ L2 @ L3 ) )
          = ( app @ ( plus @ zero @ M2 ) @ M3 @ ( app @ zero @ M2 @ nil @ L2 ) @ L3 ) ) ).
An example DH0 problem is DAT346^1. An example DH1 problem is DAT342^1.