Substructural logics and fast-growing complexities
This thesis studies how computationally difficult it is to reason in certain non-classical logical systems, and develops mathematical tools to measure that difficulty.
Part 1 looks at substructural logics, logical systems that drop some of the usual rules of classical logic (such as being able to freely reorder, repeat, or ignore information). This makes them useful for reasoning in scenarios where order and resources matter, such as computer programs, physical processes, or natural language. Whether an assertion holds in these logics can technically be decided by an algorithm, but not necessarily quickly. The thesis shows that many of them are decided only by algorithms so slow that even massively fast-growing mathematical functions—like the Ackermann function, whose outputs explode from 1 to a 20,000-digit number in just five steps—are needed to describe their difficulty. It also advances a decades-old open question about the exact difficulty of a well-known fuzzy logic system. All in all, Part 1 sheds light on the trade-off between logical expressiveness and computational complexity.
Part 2 contributes to the theory of well-quasi-orders, general-purpose mathematical tools that help prove algorithms terminate and measure how long they might take. These tools are essential to Part 1's results.
Part 3 extends a well-known technique for defining computable functions without referencing physical machines into a more abstract setting involving infinite ordinal numbers. This yields a new way of understanding a classic hierarchy of computable functions, showing precisely how using "bigger" infinities in the recursion corresponds to more computational power.