Are random axioms useful?

TL;DR

This paper examines the utility of adding random axioms, such as consistency statements, to formal theories and finds that such axioms do not significantly enhance the ability to prove new interesting theorems unless proof complexity is restricted.

Contribution

It analyzes the effectiveness of random axioms in formal theories and demonstrates their limited usefulness in proving new theorems without constraints on proof complexity.

Findings

Random axioms do not help prove new interesting theorems without proof complexity limits.

Adding consistency axioms alone is not beneficial for expanding provable statements.

The utility of random axioms is limited in the context of rich formal theories.

Abstract

The famous G\"odel incompleteness theorem says that for every sufficiently rich formal theory (containing formal arithmetic in some natural sense) there exist true unprovable statements. Such statements would be natural candidates for being added as axioms, but where can we obtain them? One classical (and well studied) approach is to add (to some theory T) an axiom that claims the consistency of T. In this note we discuss the other one (motivated by Chaitin's version of the G\"odel theorem) and show that it is not really useful (in the sense that it does not help us to prove new interesting theorems), at least if we are not limiting the proof complexity. We discuss also some related questions.