Good day everybody,
I would like to ask a question about undecidability. May I ask You, if we have some problem that is undecidable but true, for example if RH would be found out to be undecidable it would mean that it is true, does that mean that such undecidable problem is true for no reason at all, or is there some hidden pattern/reason why the statement is true, just that such pattern is inaccesible for Turing Machines?
In other worlds, if we don´t limit ourselves to proofs of finite length and we allow proofs of infinite, even uncountable length, could in such infinitary logic be constructed some proof of computably undecidable problems?
I am asking this, because I really like to think about how some hypothetical entities which would have hypercomputing minds would do mathematics. The question I would like to ask You is whether there could be those proofs of uncountable length that would constructively prove computably undecidable statements, so those entities could prove those statements formally more or less the same way we do with finite length proofs?
Of course those entities could brute force check for counterexample and "prove" those computably undecidable problems that way, but I regard this as very dumb way of getting the result and not a proof at all. So could they prove computably undecidable statements in a "smart" way with formal proofs of infinite length?
Thank You very much for Your kind answers
EDIT: Rephrasing of question: Lets have true/undecidable statement S. The way we know that it is true is because it is undecidable (if it was false, then there would be a counterexample hence it wouldn´t be undecidable).
But what makes such statement to be true? Is it a proof of infinite length which proves S from initial axioms or is it truly just an absence of a counterexample?
In other words lets have some entity E whose mental/computational capacity is that of an arbitrary powerfull hypercomputer (capable of computing truth values of all propositions in set theoretic universe V). Now could E prove that S is true in some other way than just brute force lookup for counterexample(for example if S is Rieman Hypothesis than by brute force I mean compute zeta function for all numbers and look where the zeros lie)?
So could E use for example a proof of uncountable length or property of some for TM inaccessible mathematical structure, much like properties of eliptic curves were used to prove Fermats Last Theorem?
It depends on exactly what you are asking. If you take a Turing machine, if you have an intelligently coded tape with an infinite number of possibilities encoded on it, then the halting status of all finite programs will be decidable. For a description of how this works, see Eric Holloway's "The Logical Possibility of Halting Oracles".
Short way of describing this is that there are a countably infinite number of programs on a Turing machine. If we know which ones halt, we can encode that ahead-of-time on an infinitely long tape. We can then index this infinitely long tape by the program number (which is just your program expressed as a number) and retrieve the halting status.
Now, if your question is whether or not we can prove these undecidable questions without having such answers available, again, it depends on what you mean. If you allow for a Turing machine to complete an infinite number of states, then you can check the results afterwards. So, for instance, if I am looking for Fermat's last theorem, I can do a check of all combinations of integers, and see if any of them satisfy a^n + b^n = c^n, and set a bit if it is true, and leave it unset if it is false. Then, after an infinite number of states, I can check the flag and determine if it is true.
Again, it all depends on what you will allow.
One additional note - the solution relies on the Turing machine having greater power than the problem being solved. So, for instance, in our halting example, it worked because our checking program had a program size of infinite length, while the program being checked was only finite. If we extend it so that we are checking programs of infinite length (i.e., of the same order as our checker), then we run into the halting problem again.