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!
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 theo
...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,...
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.
Mark Chimes I asked in Slack how can I grant you edit permisses, though the system doesnt seem to be in place yet. Also, check that nothing is missing in the page. I think I saw more text in the DIFF than what is now shown.
Mark Chimes I am imagining myself in the shoes of somebody who doesn't know anything about cat theory getting frustrated when they find that the article keeps talking about morphisms without giving a clue of what they are.
I think that it would be valuable to spend some time working on an intuitive definition of morphism in its corresponding page to alleviate that.
Probably you will want to precisely define morphism at some point, but I recommend you do it sooner rather than later to enforce coherence.
Alexei I was aiming for the Python syntax of the ternary operator, but I am still quite unfamiliar with Arbital and I do not know how to format it nicely.
Also, is quite a funny situation that even though I am the creator and maintainer I do not have privileges to edit the page. Is that intentional?
This is redacted in a very confusing way.
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!
Yup, some people seem to think that one of the correct moves in 'coming to agreement' is that our probabilities begin to average out. (I have another’s post on this drafted.)