Suppose we have an axiom system and theorems derived out of that axiom system, is there any way to rigorously speak about a theorem being more difficult to prove than others?
In my personal thoughts, I think maybe we can take the difficulty to prove the theorem as in the number of steps in the shortest proof of it... but a disadvantage of this way is that it maybe that a longer proof is actually a psychologically easier to understand.
Are there other ways?
Motivation
Suppose in the future that for some reason that we derive a contradiction from the existing foundation of mathematics then I was contemplating how one could try to salvage it into something which is still contradiction free.
A thought which come in this contemplation was, Would the theorems of lesser difficulty, for a suitable definition of difficulty, be more possible to retains than others in the salvaged axiom system?
Example: I am thinking of a situation like the day when Russel Paradox was discovered. If I have understood it correctly, the issue was stemmed out of how the axiom of comprehension was written.
The interesting thing was that even when ZFC came, we were able to implement many of the conceptual ideas we had in Set theory in the Naive set theory back in it. So, the thought was, could there be a way to quantify the difficulty so that we could say think things like "hmm these theorems would could survive even if the foundations were a bit different".
Tangentially related question on Philosophy.SE and Reverse Mathematics: figuring out what axioms a theorem is equivalent too