Abstracts.2018.FixpointTheoriesFOL

Fix-point theories in first order logic

by Mattias Granberg Olsson

In this talk we will consider two theories of (non-iterated) fix-points over a base theory, in classical and intuitionistic first order logic respectively. Following the basic definitions I will introduce the problem of (my) interest, namely that of conservativity over the base theory. It is known that the intuitionistic variant (and stronger theories) is conservative over HA, while the classical one is not conservative over PA. After a brief discussion of the history of the positive result, I will present work in progress on a new idea for a proof of this fact, or fragments of it.