This is rather random, but I really appreciate the work made by the moderators when explaining their reasons for curating an article. Keep this up please!
Jaime Sevilla Molina
Karma: 70
Epoch AI is hiring a CTO!
Data on AI
Epoch is hiring an ML Distributed Systems Senior Researcher
Announcing Epoch’s newly expanded Parameters, Compute and Data Trends in Machine Learning database
Might as well do it! No promises though.
My fault, it should be \ulcorner.
The problem I have in mind is deciding whether the Halting problem is equivalent to any statement of the form “You cannot decide membership for ”, where is a non-trivial set of computable functions.
Clearly the argument exposed above shows that the Halting problem implies any of these statements, but does the reverse implication hold directly? In my proof of how Rice implies Halting I am handpicking an . Can we make do without the handpicking?
In other words, given a Halting oracle, can we make a Rice oracle for an arbitrary ?
Out of curiosity, is there any reason you are avoiding calling this lemma by its traditional name, Euclid’s lemma?
Generalized fixed point theorem:
Suppose that are modal sentences such that is modalized in (possibly containing sentence letters other than ).
Then there exists in which no appears such that .
We will prove it by induction.
For the base step, we know by the fixed point theorem that there is such that
Now suppose that for we have such that .
By the second substitution theorem, . Therefore we have that .
If we iterate the replacements, we finally end up with .
Again by the fixed point theorem, there is such that .
But as before, by the second substitution theorem, .
Let stand for , and by combining the previous lines we find that .
By Goldfarb’s lemma, we do not need to check the other direction, so and the proof is finished
An immediate consequence of the theorem is that for those fixed points and every , .
Indeed, since is closed under substitution, we can make the change for in the theorem to get that .
Since the righthand side is trivially a theorem of , we get the desired result.
One remark: the proof is wholly constructive. You can iterate the construction of fixed point following the procedure implied by the construction of the to compute fixed points.
Pedantic remark: Aren’t you missing the identity of free groups in your intuitive construction?
We have the and the . Where is ?
I do not think that the “Me facing off against 99 CDT agents and 1 LDT agent, versus an LDT agent facing 99 LDT agents and 1 CDT agent” is fair either.
The thing that confuses me is that you are changing the universe in which you put the agents to compete.
To my understanding, the universe should be something of the form “{blank} against a CDT agent and 100 LDT agents in a one-shot prisoners dilemma tournament”, and then you fill the “blank” with agents and compare their scores.
If you are using different universe templates for different agents then you are violating extensionality, and I hardly can consider that a fair test.
I fail to see how this setup is not fair—but more importantly, I fail to see how LDT is losing in this situation. If the payoff matrix is CC:2/2, CD:0/3, DD: 1⁄1, then if LDT cooperates in every round it will get utilons, while if it defected then it gets utilons.
Thus wins utilons in this situation, while a CDT agent in his shoes would win utilons by defecting each round.
The situation changes if the payoff becomes Having a higher score that CDT: , while Having an equal or lower score than CDT: .
Then the game is clearly rigged, as there is no deterministic strategy that LDT could follow that would lead to a win. But neither could CDT win if it was pitted in the same situation.
Uniqueness of arithmetic fixed points:
Notation:
Let be a fixed point on of ; that is, .
Suppose is such that . Then by the first substitution theorem, for every formula . If , then , from which it follows that .
Conversely, if and are fixed points, then , so since is closed under substitution, . Since , it follows that .
(Taken from The Logic of Provability, by G. Boolos.)
“Formula” and “Statement” can be interchanged freely.
Both refer to well-formed strings in the language of interest, in this case the language of arithmetic ( and the logical symbols).
Yeah, that is the formal definition of the standard provability predicate. I’ll add the page explaining that soon enough.
I think that the clickbait and the summary should be exchanged.
I’ll try to cover probabilistic Turing machines in other article once I have time. Thanks for your interest!
I love the effect, but I would drop one of the ’as much’s for increased lyricism.
I appreciate that in the example it just so happens that the person assigning a lower probability ends up assigning a higher probability that the other person at the beginning, because it is not intuitive that this can happen but actually very reasonable. Good post!