Expressing versus Proving: Relating Forms of Complexity in Logic

Complexity in logic comes in many forms. 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 the non-deterministic logspace complexity class) and its totality (and, thus, the closure of NL under complementation) is provable within NL-reasoning. Lastly, we will touch upon the topic of formalizing complexity theory using logic, and the meta-question of complexity of logical reasoning about complexity-theoretic statements. This is intended to be a high-level overview, suitable for readers who are not familiar with complexity theory and complexity in logic.