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 | φ,ψ | Φ,Ψ |