This 2 hour lecture gives a survey on the expressive power of numerical
predicates. In particular, the following logics are considered:
(1) First-order logic with Bit-predicate (FO(Bit), for short):
It is well-known that the linear order can be expressed in FO(Bit)
and that FO(Bit) is exactly as expressive as, e.g., first-order logic with
addition and multiplication or, equivalently, first-order logic with addition
and a "square numbers" predicate.
In this talk I will also sketch the proof of a not so well-known result
stating that there are 5 particular linear ordering relations such that
FO(Bit) is exactly as expressive as first-order logic with these five
linear orders.
(2) First-order logic and monadic logics with addition (FO(+), MLFP(+), MSO(+)):
I will present an Ehrenfeucht-Fraisse game proof of the Theorem of Ginsburg and Spanier,
stating that FO(+)-sentences have semi-linear spectra.
Concerning extensions of FO(+) which allow quantification of monadic relations, it is
known that on strings with built-in addition, monadic second-order logic MSO(+)-sentences
can describe exactly those languages that belong to the linear time hierarchy.
Furthermore, it is known that monadic least fixed-point logic MLFP(+) can describe
at least all problems in Grandjean's linear time complexity class DLIN.
This, in particular, leads to a result stating that a separation between the expressive
power of addition-invariant MLFP(+) and addition-invariant MSO(+) on strings would imply
a separation between the complexity class DLIN and the linear time hierarchy.
Apart from these topics, I will also survey results on
(3) first-order logic with counting quantifiers and various numerical predicates
and
(4) the Crane Beach conjecture.