Edit abstract data

### Abstract

There are many ways to define complexity in logic. In
finite model theory, it is the complexity of describing properties,
whereas in proof complexity it is the complexity of proving properties
in a proof system. Here we consider several notions of complexity in
logic, the connections among them, and their relationship with
computational complexity. In particular, we show how the complexity of
logics in the setting of finite model theory is used to obtain results
in bounded arithmetic, stating which functions are provably total in
certain weak systems of arithmetic. For example, the transitive
closure function (testing reachability between two given points in a
directed graph) is definable using only NL-concepts (where NL is
non-deterministic log-space complexity class), and its totality is
provable within NL-reasoning.