For use in theory, it simplifies reading formulas when we stick to a general convention for naming variables of a particular type. Those naming conventions for symbols are summarized in the following table. For practical purpose, of course, those naming conventions are non-rigid but arbitrary names are supported. Then the types are resolved by declaration.
| Level | Kind of symbol | Type | constant | variable | ||
|---|---|---|---|---|---|---|
| arity>0 | arity=0 | arity>0 | arity=0 | |||
| language | Function symbol | σ→τ |
f,g,h | a,b,c | x,y,z | |
| Predicate symbol | (σ) |
p,q,r | ||||
| meta language | Formula | meta | φ,ψ | Φ,Ψ | ||