I have some error: from the below it follows that if the formal system found is distinct from the original one then it’s provable that the input algorithm does not halt (if it halts, it’s provable that it halts in Peano arithmetic) and therefore we have an algorithmic solution of halting problem.
It’s well known that halting problem (whether a given algorithm ever stops) is not algorithmically solvable.
I will show that halting problem is indeed “essentially” solvable in some sense.
Given a formal system containing Peano arithmetic (e.g. Peano arithmetic itself), by my previous article, there is a (fixed) algorithm that finds a minimal (non-contradictory) formal system where it’s provable that the input algoritm halts or that it doesn’t halt.
So, if we consider every non-contradictory formal system “above” some fixed formal system “valid”, then halting problem has a valid algorithmic solution in it.
Remark: Considering every formal system valid recalls the philosophy of relativism. However, should to note the easy truth that “everything being relative” is itself a relative truth.