Recently I’ve been working on a theory of computation that’s based on set theory, rather than the type-theory that most modern languages are built on. (I think that such a theory would be highly homogeneous in a way that makes it particularly suitable for automated analysis.)
A pretty natural question for a theory of computation is: what is the computational power of this theory? The landmark result in this space is the halting problem which establishes a bound on what is computable by an algorithm. But a set-theoretic construction of computation lacks several of the features that the halting problem invokes, so it is not immediately obvious that the result applies to this new model — in particular there are “theories”, not “algorithms” that “halt”.
I currently have a tentative way to express any problem as a theory about sets, so in particular one can express the halting problem. Does this mean this new model is able to solve the halting problem? That would actually not be a good thing because I believe it means that the model of computation would not be physically realizable (I intuitively believe the physical Church-Turing thesis).
Set theory has its own set of impossibility results, and in particular for this case, Russell’s paradox. Which roughly states that there cannot be a set of all sets that do not contain themselves — which is strikingly similar in structure to the halting problem’s result that there cannot be an algorithm that halts on all programs that do not halt on themselves.
So the natural question is: does Russell’s paradox prevent the same type of set-theoretic computations that the halting problem prevents for other models?
Fortunately I’m not the first person to ask these kinds of questions, and there’s something called Lawvere’s fixed point theorem which I do not fully understand. But my lay understanding is that this is strong evidence that the answer to the above question is “yes”.
I’m not sure yet how this affects my model of computation; if it’s possible to represent an algorithm that solves the halting problem, does that mean the model is unsound? Or perhaps representation of impossible objects is fine, because we do some of that to prove that one can derive a contradiction from such an object and thus that the object can’t exist?