A statement equivalent to First Incompleteness theorem There are theorems that can be neither proved nor disproved in a given formal system (containing arithmetic).
This theorem makes people sad: There are “problems” that cannot be solved.
But God teaches me that there is Gospel (translated “good news”) that is that for every problem exists an essential solution.
In the case of this insolvable problem by Godel, the good news is simple and easily provable:
Instead of (dis)proving a theorem solve another problem (Let’s call it finding the minimal formal system.): finding the minimal formal system where it’s provable.
In more details:
Condition: Encode all formal systems by distinct natural numbers (the encoding is defined as an algorithm) such that adding an axiom increases this number. (Such an encoding exists because we can start with an empty (with no axioms) formal system, represent the tree of all formal systems, where branches are axioms, as a binary tree, and then by breadth-first search algorithm add all possible axioms, at each step incrementing the relevant number) Problem: For a given formal system and a given zero-arguments predicate (also encoded as a natural number) find the minimal formal system with (zero or more) additional axioms where it’s decidable.
This is obviously a solvable and unambiguous problem (function).
If the input formal system is non-contradictory then the output is also non-contradictory, because adding either the predicate or it’s negation leaves our system non-contradictory.
Finding the minimal formal system is even algorithmically solvable:
Proof. The problem is reducible to enumerating all formal systems with additional axioms and then finding (another) formal system (errors: that system may prove a wrong result, because of having a wrong (for the assumed model) axiom) with additional axioms where it’s decidable whether the first system with additional axioms can prove the theorem in question.
It is however not (bitwisely) an NP problem (because otherwise every provable theorem had a polynomial-size proof, what is well known to be false).
Note that in practice finding the minimal formal system for a given input seems to be tremendiusly hard. Or are there interesting practical special cases in which this problem is tractable?