[Solved]: How does the use of oracle Turing machines not lead to contradictions?

There’s a number of ways to look at this. One is that in proofs, implication is kind of like a function, that takes as input a proof of something, and outputs a proof of something else. We can write functions that operate on values that we don’t have. For example, let’s consider the halting number $h$, which is not computable. I can write the function $haltingPlusOne : {h } rightarrow mathbb{N}$ $haltingPlusOne(x) = x + 1$. This function takes as input the Halting number, and returns the Halting number plus one. Clearly this is a well defined function: if we give it the right input, it gives the right output. The fact that we can’t find the right input doesn’t make it any less valid of a transformation. I see proofs with oracles as similar. They’re basically functions which say, give me a Turing machine that solves problem $X$, and I’ll give as output a proof of some theorem. It’s also important to realize that when we say something like “There is no Turing Machine that can decide the halting problem,” that is saying that, there’s no TM matching the standard definition of a TM that decides the halting problem. An oracle is basically saying “Assume we have a TM that matches the normal definition except also assuming we can solve some problem”. So there’s no contradiction, since we’re not assuming there’s a normal TM accepting the problem, we’re assuming there’s a special TM accepting the problem. In a very informal analogy, think of it like this. If I can prove to you that no humans without superpowers can fly, there’s no contradiction saying that there’s a superhero that can fly. These oracles are purely logical objects. We don’t know how to build physical machines that emulate them, the way we can with Turing machines, but as far as we know, there’s no inherent contradiction between their definitions and our basic axioms. As logical objects, these oracles do exist. We know they’re not standard Turing Machines or Lambda-Calculus terms or Partial-recursive functions. The Church-Turing thesis says that there’s no more powerful model, but it’s not a theorem, it’s just a conjecture, and is too informal to ever really be proved.