A Note on the Decidability of the Necessity of Axioms

TL;DR

This paper investigates the decidability of determining whether an axiom is necessary for a proof within a logical system, showing that this problem is generally undecidable unless a related system is decidable.

Contribution

It establishes a new undecidability result for the problem of axiom necessity in mathematical logic, linking it to the decidability of related systems.

Findings

Necessity of axioms problem is undecidable in general.

Decidability depends on the decidability of the system with the negation of the axiom.

Provides conditions under which the problem becomes decidable.

Abstract

A typical kind of question in mathematical logic is that for the necessity of a certain axiom: Given a proof of some statement $\phi$ in some axiomatic system $T$, one looks for minimal subsystems of $T$ that allow deriving $\phi$. In particular, one asks whether, given some system $T+\psi$, $T$ alone suffices to prove $\phi$. We show that this problem is undecidable unless $T+\neg\psi$ is decidable.