Is it possible that "hard mathematical problems" would be easier in some other axiom systems?

Question

Is it possible that "hard mathematical problems" would be easier in some other axiom systems?

Does this make any sense?

I was motivated by this question after reading some paper that concerned how the choice of axiom system affects "attainable truths". Thus while some questions may be unanswerable given some axioms, they might be attainable using some other.

Answer 1

Taken literally this question has a trivial answer: any question is answerable in a theory which has an answer to that question as an axiom.

However, this isn't the only way new axioms can help answer a question: we can have a situation where $\varphi$ is provable in $T$, but only via very messy proofs, whereas $\varphi$ is much easier to prove in $T+\sigma$. This raises the question:

When do we know that $(i)$ $T$ and $T+\sigma$ prove the same sentences in class $\mathfrak{S}$, but $(ii)$ some sentences in $\mathfrak{S}$ are much easier to prove in $T+\sigma$ than in $T$?

(This is related to the notion of conservative extensions.)

"Easier" here could be understood in terms of length or in terms of intuition. For an example of how these can play out differently, consider Shoenfield absoluteness. Shoenfield tells us (for example) that any $\Pi^1_2$ sentence which is provable from $\mathsf{ZFC+GCH}$ is provable from $\mathsf{ZF}$. Now this may help a lot with intuition, since $\mathsf{ZFC+GCH}$ gives us a lot of powerful techniques for finding proofs, but it won't help with length substantially: we can translate a $\mathsf{ZFC+GCH}$ proof into a $\mathsf{ZF}$ proof by just relativizing to $L$ and then quoting Godel and Shoenfield. This is very little overhead: basically linear in the length of the statement being proved (rather than the proof itself). (On the other hand, Godel's speedup theorem shows that we can have length improvements in other situations.)

Answer 2

Perhaps this is not exactly what you are looking for, but it can be interesting to know: there is a kind of a category called "topos" that has intuitionistic logic (= classical logic without Law of Exluded Middle) as its "internal logic". The category of sets and the category of sheaves are examples of toposes.

The internal language of a topos can be used to simplify proofs. In homological algebra, this can be seen in Johnstone's book "Topos Theory" when he proves that the category $Ab(E)$ of group objects of a topos $E$ is abelian. Besides that, Ingo Blechschmidt's Thesis is all about using the internal logic of the Zariski topos in Algebraic Geometry.