On several occasions, the authors emphasize how the intuitive nature of "effective computability" renders futile any attempt to formalize the thesis. However, I'm rather interested in formalizing intuitive concepts and therefore wondered why this hasn't been attempted.
Formalizing the intuitive notion of effective computability was exactly what Turing was trying to do when he introduced Turing machines, and Turing's thesis claims that his attempt was successful. If you come up with a new formalization of effective computability and prove it equivalent to Turing computability, then in order to use this as a proof of Turing's thesis, you would need to argue that your new formalization is correct. But such an argument would inevitably be informal, since it links a formal concept to an informal concept, and there already have been informal arguments for Turing's thesis, so I don't think there is anything really fundamental to be gained from this.
Another way of putting it: you can't possibly know that there isn't some device out in the universe that lets you do more powerful things than your model (eg. a device that can tell you whether an arbitrary Turing machine halts), so it can never be proven that your model captures real-world computability.
Fwiw, I disagree with the frame of that post as well.
I'm happy to agree that you can prove that your model captures real-world computability under a particular formalization of physics.
Consider the halting set; ... is not enumerable / computable.
...
Here, we should be careful with how we interpret "information". After all, coNP-complete problems are trivially Cook reducible to their NP-complete counterparts (e.g., query the oracle and then negate the output), but many believe that there isn't a corresponding Karp reduction (where we do a polynomial amount of computation before querying the oracle and returning its answer). Since we aren't considering complexity but instead whether it's enumerable at all, complementation is fine.
You're using the word "enumerable" in a nonstandard way here, which might indicate that you've missed something (and if not, then perhaps at least this will be useful for someone else reading this). "Enumerable" is not usually used as a synonym for computable. A set is computable if there is a program that determines whether or not its input is in the set. But a set is enumerable if there is a program that halts if its input is in the set, and does not halt otherwise. Every computable set is enumerable (since you can just use the output of the computation to decide whether or not to halt). But the halting set is an example of a set that is enumerable but not computable (it is enumerable because you can just run the program coded by your input, and halt if/when it halts). Enumerable sets are not closed under complementation; in fact, an enumerable set whose complement is enumerable is computable (because you can run the programs for the set and its complement in parallel on the same input; eventually one of them will halt, which will tell you whether or not the input is in the set).
The distinction between Cook and Karp reductions remains meaningful when "polynomial-time" is replaced by "Turing computable" in the definitions. Any set that an enumerable set is Turing-Karp reducible to is also enumerable, but an enumerable set is Turing-Cook reducible to its complement.
The reason "enumerable" is used for this concept is that a set is enumerable iff there is a program computing a sequence that enumerates every element of the set. Given a program that halts on exactly the elements of a given set, you can construct an enumeration of the set by running your program on every input in parallel, and adding an element to the end of your sequence whenever the program halts on that input. Conversely, given an enumeration of a set, you can construct a program that halts on elements of the set by going through the sequence and halting whenever you find your input.
Thanks, my terminology was a little loose. What I was trying to hint at is that some of the paradox's culling operations require uncomputable tests of English sentences, and that the regularity of the original language doesn't determine the status of its subsets.
But that's not what the puzzle is about. There is nothing about computability in it. It is supposed to be a paradox along Russell's set of all sets that don't contain themselves.
The response about formalizing exactly what counts as a set defined by an English sentence is exactly correct.
But there are more objections; even if "computability" isn't explicitly mentioned in the problem, it's still present. Are the sets "the singleton set containing 1 if and only if machine halts on input " and "the singleton set containing 1" the same? Even if we grant a procedure for figuring out what counts as a set, we can't even compute which sentences are duplicates.
That still doesn't make computability relevant until one introduces it deliberately. Compare to weaker notions than computability, like computability in polynomial time. Computability theory also complains the same once we have explicitly made definability subjective, and should have no more logical problems.
Saying that the problem is about computability because there is no computable solution proves too much: I could reply that it is about complexity theory because there is no polynomial-time solution. (In fact, there is no solution.)
We can build something like a solution by specifying that descriptions must be written in some formal language that cannot describe its own set of describables, then use a more powerful formal language to talk about that previous language's set. For powerful enough languages, that's still not computable, though, so computability theory wouldn't notice such a solution, which speaks against looking at this through the lens of computability theory.
Sure, but how do we get the final set, then? The paradox addresses the reader in the imperative, implying one can follow along with some effective procedure to trim down the set. Yet if Turing’s thesis is to be believed, there is no such procedure, no final set, and therefore no paradox.
Computability is just \Delta^0_1 definability. There are plenty of other notions of definability you could try to cash out this paradox in terms of. Why pick \Delta^0_1 definability?
If the argument worked in any particular definability notion (e.g. arithmetic definability) it would be a problem. Thus, the solution needs to explain why the argument shouldn't convince you that with respect to any concrete notion of definable set the argument doesn't go through.
It seems "Computability and Logic" doesn't include Kleene's recursion theorem and Rice's theorem. What sources would you recommend for learning those theorems, their proofs, and their corollaries? Also, which chapters of "Computability and Logic" are required to understand them?
Michael Sipser's Introduction to the Theory of Computation goes over the recursion theorem and Rice's theorem, IIRC. The proofs are given as well as associated exercises. The textbook walks you through, from DFAs to Turing Machines, so it's pretty self-contained, if you're looking at a source other than Computability and Logic to understand them.
Foreword
Max Tegmark's Our Mathematical Universe briefly touches on a captivating, beautiful mystery:
The profound results compiled by the Computability and Logic textbook may be the first step towards the answer.
Computability and Logic
As usual, I'll explain confusions I had and generally share observations. This book is on the MIRI reading list.
1 Enumerability
Coming back to this book, I'm amazed by some of my margin scribbles – expressions of wonderment and awe at what now strike me as little more than obvious facts ("relations are sets of ordered pairs!").
2 Diagonalization
Exercise 2.13 (Richard's paradox) What (if anything) is wrong with following argument?
My first time reading this exercise, I had plenty of objections. "Is not abusive to use English in place of a formal system? How do we even quantify the expressiveness of English, is that a thing?", and so on. Yet, returning with more context and experience, a few minutes thought revealed to me the crux: information and enumerability aren't just defined by what is present, but by what's not.⋆
Let's take a little detour. Consider the regular expression 1∗; its language is infinite, and certainly computable. We don't even need a Turing machine to recognize it; a strictly less-expressive finite state automaton would do just fine. And yet there are infinite subsets of this language which are not at all computable.
Consider some reasonable encoding ⟨M,w⟩ of a Turing machine M and input w. As we see later, we can enumerate all possible Turing machines and inputs (given that we first fix the alphabet, etc.). This means that we can number the encodings. Consider the halting set; that is, {⟨M,w⟩|M halts on input w}. Expressed in unary, the numbers of the encodings belonging to this set is a strict subset of the regular language 1∗, and yet is not computable (because the halting set is not negatively recursively semi-decidable; i.e., we can't say a computation won't halt. Thus, its complement is not computable).
Do you see the problem now?
⋆ Here, we should be careful with how we interpret "information". After all, coNP-complete problems are trivially Cook reducible to their NP-complete counterparts (e.g., query the oracle and then negate the output), but many believe that there isn't a corresponding Karp reduction (where we do a polynomial amount of computation before querying the oracle and returning its answer). Since we aren't considering complexity but instead whether it's computable at all, complementation is fine.
3 Turing Computability
On several occasions, the authors emphasize how the intuitive nature of "effective computability" renders futile any attempt to formalize the thesis. However, I'm rather interested in formalizing intuitive concepts and therefore wondered why this hasn't been attempted. Indeed, it seems that a recent thesis by Vinogradova conducts a category-theoretic formalization of the notion of abstract computability (although since I don't yet know category theory, I can't tell how related it is).
4 Uncomputability
5 Abacus Computability
6 Recursive Functions
Nate wrote:
However, the book defines minimization like so:
This confused me for days, and I didn't truly understand it until I came back several months later (i.e., now). How in the world is it effectively computable if it isn't even defined on all inputs?
Suppose I challenge you to give me a function that, given a number x, returns a larger number. The catch is that you aren't allowed to directly modify x – you can only use it to check whether your candidate solution is bigger. If you just use the bounded search provided by primitive recursion, for some valid inputs your function will be wrong. If you have to start from scratch, there's no finite number of exponentiations or tetrations or super-duper-tetrations that you can include which will work for all inputs. You have to be able to do unbounded search – for example, taking the successor until you get a larger number.
Depending on the domain, this isn't always total, either. If we're working with R+ and I give you ∞, you'll increment forever. Similarly, your function won't be defined on input cat. The important part is that we've given an effective procedure for finding the solution whenever it exists and for valid inputs.
7 Recursive Sets and Relations
8 Equivalent Definitions of Computability
Coming to appreciate this bridge between math and computer science was one of my most profound experiences last year. My mind's eye began viewing the world differently. Goings-on came to be characterized not just as interactions of atomic "objects", but as the outgrowth of the evolution of some mathematical structure. As a vast and complex play of sorts, distorted by my mind and approximated in specific ways – some legible, others not.
Most of all, a tugging in the back of my mind intensified, continually reminding me just how ignorant I am about the nature of our world.
9 A Précis of First-Order Logic: Syntax
10 A Précis of First-Order Logic: Semantics
I can't emphasize enough how helpful Nate's Mental Context for Model Theory was; the mental motions behind model theory are a major factor in my excitement for studying more logic.
11 The Undecidability of First-Order Logic
12 Models
Coming out of linear algebra with a "isomorphism ?= bijection" confusion, the treatment in this chapter laid the conceptual foundation for my later understanding homomorphisms. That is, a key part of the "meaning" of mathematical objects lies not just in their number, but in how they relate to one another.
This chapter is also great for disassociating baggage we might naïvely assign to words on the page, underlining the role of syntax as pointers to mathematical objects.
13 The Existence of Models
14 Proofs and Completeness
15 Arithmetization
16 Representability of Recursive Functions
I confess that upon wading back into the thicket of logical notation and terminology, I found myself lost. I was frustrated at how quickly I'd apparently forgotten everything I'd worked so hard for. After simmering down, I went back through a couple chapters, and found myself rather bored by how easy it was. I hadn't forgotten much at all – not beyond the details, anyways. I don't know whether that counts as "truly a part of me", but I don't think it's reasonable to expect myself to memorize everything, especially on the first go.
17 Indefinability, Undecidability, Incompleteness
Indeed, the notion of provability can be subtly different from our mental processes for judging the truth of a proposition; within the confines of a formal system, provability doesn't just tell us about the proposition in question, but also about the characteristics of that system. This must be kept in mind.
18 The Unprovability Of Consistency
19 Normal Forms
20-27 [Skipped]
I found these advanced topics rather boring; the most important was likely provability logic, but I intend to study that separately in the future anyways.
Final Thoughts
I really liked this book. In the chapters I completed, I did all of the exercises – they seemed to be of appropriate difficulty, and I generally didn't require help.
I've already completed Understanding Machine Learning, the first five chapters of Probability Theory, and much of two books on confrontational complexity. I'm working through a rather hefty abstract algebra tome and intend to go through two calculus books before an ordinary differential equations text. The latter material is more recreational, as I intend to start learning physics. This project will probably be much slower, but I'm really looking forward to it.
Forwards
I don't think I'm a great mathematician yet by any means, but as my studies continue, I can't shake a growing sense of structure. I'm trying to broaden my toolbox as much as possible, studying areas of math which had seemed distant and unrelated. Yet the more I learn, the more my mental buckets collapse and merge.
And to think that I had once suspected the Void of melodrama.
If you are interested in working with me or others to learn MIRI-relevant math, if you have a burning desire to knock the alignment problem down a peg - I would be more than happy to work with you. Message me for an invitation to the MIRIx Discord server.