Some abstract versions of G\"odel's second incompleteness theorem based on non-classical logics

TL;DR

This paper explores generalized forms of G"odel's second incompleteness theorem within non-classical logics, highlighting the importance of contraction rule and providing examples where G"odel's argument fails.

Contribution

It introduces abstract versions of G"odel's theorem for weaker logics and analyzes the role of contraction, offering new insights into logical foundations.

Findings

Generalizations of L"ob's derivability conditions for non-classical logics

Identification of contraction rule's role in G"odel's theorem

Example of modal logic system without contraction invalidating G"odel's argument

Abstract

We study abstract versions of G\"odel's second incompleteness theorem and formulate generalizations of L\"ob's derivability conditions that work for logics weaker than the classical one. We isolate the role of contraction rule in G\"odel's theorem and give a (toy) example of a system based on modal logic without contraction invalidating G\"odel's argument.