This makes me consider a second loophole: even with, for a given set of axioms, we cannot prove some given P does not halt (Godel's incompleteness theorems). Ho

This makes me consider a second loophole: even with, for a given set of axioms, we cannot prove some given P does not halt (Godel's incompleteness theorems). However, that makes us wonder if there can be a procedure that suggests stronger, but still minimal axioms (consistent with say Peano arithmetic or ZFC) and proves them in this new axiomatic basis? (1) Would this proof be considered acceptable? (or can we devise a system that guarantees found proofs to be acceptable) (2) Is this procedure feasible? If anyone has literature on this topic, this is interesting! (an optimistic alternative to incompleteness)