You kind of just have to assume that the interpreter works, and your computer wasn’t hit by a cosmic ray that flipped a random bit invalidating your proof. You can try some sort of probabilistic thing, but with what interpreter do you define your probabilities? There is no probabilistic Loeb’s theorem. Once you take the leap of faith though, you can build your interpreter by assuming you have some number of bits and NAND gates, and asking what circuits you can make. Then you can write finite programs that prove things about the relationships between different strings of bits. There are many similar kinds of interpreters (e.g. rather than NAND gates, a human chooses a set of ‘logical operators’, writes them down on paper, and runs the program through with their brain).
Yes, the correspondence is the other way. See the paragraph after the one you quoted. I think my earlier self was wrong, though there is the possibility I just cannot reconstruct their thought process.
I don’t understand why you are talking about interpreters. Do you agree that the Y combinator, when applied to a lambda function, might not be a lambda function corresponding to a number? Or, say, a lambda function that encodes the set in question? I still don’t see how you are encoding the set in question—are you literally manipulating first order logic strings encoded as numbers? If so, then once again you might get a fixed point that corresponds to no number—and even if you get a number, the encoded string might not correspond to a set.
To clarify 2 (though I think we don’t disagree here) - the reason you stop at the universal cover is simply because that’s where you get a bijection.
I thought you were asking about interpreters: “And also, how are you interpreting, exactly??” I guess not. So, I think there’s some confusion about the Y combinator here. Consider the factorial function:
iter(n) = n * iter(n-1) if n > 0 else 1
factorial = Y(iter)
You might encode n as a Church numeral. In this particular case, factorial(n) can also be beta-reduced to a Church numeral. Note though, that factorial itself is not a Church numeral. Now, consider the Serpinski triangle
iter(S) = S + (1 + w + w^2)(S/3) ; S + three dilated copies
serpinski = Y(iter)
You have some notion of how sets S should be encoded, and you are worried that serpinski(S) may not beta-reduce to fit that notion. Perhaps then you’ve got the wrong notion of sets, and should expand it to include objects like serpinski(S). But perhaps that leads to nasty problems like Russell’s paradox. I’m not sure, but I suspect you won’t run into this problem.
“To clarify 2 (though I think we don’t disagree here) - the reason you stop at the universal cover is simply because that’s where you get a bijection.”
Sorry, what bijection? Between the lifted rotations and… what?
Well, you really have F = lambda f,n: n * f(n-1) if n > 0 else 1, and then (YF)(n) beta-reduces to a church numeral. Our fixed point is the factorial function.
Trying to duplicate this with the sets in question: how should sets be encoded? I suspect that for any reasonable notion, you will have a problem where the fixed point might be some terrible thing.
As an example, suppose you try the most obvious way: a set is represented by a function that returns true for all elements in the set, and false otherwise. But how are we to plug in real numbers? Well, we could take computable approximations to the reals… but then we can’t even define the set {0} as a computable function! Even if we don’t allow something as pathological as the reals, decidable sets are much lesser than all the sets.
Any other way would, I think, have to basically be manipulating formal logic strings represented via e.g. a godel numbering and church numerals. Then, one defines the iteration as a function that takes in a string defining a set in first order logic, then outputs a first order logic string defining of the next iteration. But then, there’s no guarantee that the fixed point is a number, let alone a number corresponding to a logical formula that defines a set.
About the representations: in the finite dimensional case, there is a bijection between projective irreps of G and determinant 1 ordinary irreps of the universal cover of G. Apparently in the infinite dimensional case, you can only lift projective irreps to ordinary irreps in certain cases which include the Poincare group. I can’t tell if you would get a bijection in those cases.
I would be surprised if the motivation for projective irreps does not also motivate extending higher up the Postnikov tower; you don’t just stop at the universal cover.
As for sets, suppose you went with the definition: any function that takes in a rational number and spits out a boolean. So the Dedekind cut for could be expressed as
sqrt2 = lambda x. (x * x < 2)
I expect that
((serpinski sqrt2) 3/4)
could indeed be -reduced to a boolean, if you choose the right path. So basically, (serpinski S) is also a set if S is a set.
You kind of just have to assume that the interpreter works, and your computer wasn’t hit by a cosmic ray that flipped a random bit invalidating your proof. You can try some sort of probabilistic thing, but with what interpreter do you define your probabilities? There is no probabilistic Loeb’s theorem. Once you take the leap of faith though, you can build your interpreter by assuming you have some number of bits and NAND gates, and asking what circuits you can make. Then you can write finite programs that prove things about the relationships between different strings of bits. There are many similar kinds of interpreters (e.g. rather than NAND gates, a human chooses a set of ‘logical operators’, writes them down on paper, and runs the program through with their brain).
Yes, the correspondence is the other way. See the paragraph after the one you quoted. I think my earlier self was wrong, though there is the possibility I just cannot reconstruct their thought process.
I don’t understand why you are talking about interpreters. Do you agree that the Y combinator, when applied to a lambda function, might not be a lambda function corresponding to a number? Or, say, a lambda function that encodes the set in question? I still don’t see how you are encoding the set in question—are you literally manipulating first order logic strings encoded as numbers? If so, then once again you might get a fixed point that corresponds to no number—and even if you get a number, the encoded string might not correspond to a set.
To clarify 2 (though I think we don’t disagree here) - the reason you stop at the universal cover is simply because that’s where you get a bijection.
I thought you were asking about interpreters: “And also, how are you interpreting, exactly??” I guess not. So, I think there’s some confusion about the Y combinator here. Consider the factorial function:
You might encode
nas a Church numeral. In this particular case,factorial(n)can also be beta-reduced to a Church numeral. Note though, thatfactorialitself is not a Church numeral. Now, consider the Serpinski triangleYou have some notion of how sets
Sshould be encoded, and you are worried thatserpinski(S)may not beta-reduce to fit that notion. Perhaps then you’ve got the wrong notion of sets, and should expand it to include objects likeserpinski(S). But perhaps that leads to nasty problems like Russell’s paradox. I’m not sure, but I suspect you won’t run into this problem.“To clarify 2 (though I think we don’t disagree here) - the reason you stop at the universal cover is simply because that’s where you get a bijection.”
Sorry, what bijection? Between the lifted rotations and… what?
Well, you really have F = lambda f,n: n * f(n-1) if n > 0 else 1, and then (YF)(n) beta-reduces to a church numeral. Our fixed point is the factorial function.
Trying to duplicate this with the sets in question: how should sets be encoded? I suspect that for any reasonable notion, you will have a problem where the fixed point might be some terrible thing.
As an example, suppose you try the most obvious way: a set is represented by a function that returns true for all elements in the set, and false otherwise. But how are we to plug in real numbers? Well, we could take computable approximations to the reals… but then we can’t even define the set {0} as a computable function! Even if we don’t allow something as pathological as the reals, decidable sets are much lesser than all the sets.
Any other way would, I think, have to basically be manipulating formal logic strings represented via e.g. a godel numbering and church numerals. Then, one defines the iteration as a function that takes in a string defining a set in first order logic, then outputs a first order logic string defining of the next iteration. But then, there’s no guarantee that the fixed point is a number, let alone a number corresponding to a logical formula that defines a set.
About the representations: in the finite dimensional case, there is a bijection between projective irreps of G and determinant 1 ordinary irreps of the universal cover of G. Apparently in the infinite dimensional case, you can only lift projective irreps to ordinary irreps in certain cases which include the Poincare group. I can’t tell if you would get a bijection in those cases.
I would be surprised if the motivation for projective irreps does not also motivate extending higher up the Postnikov tower; you don’t just stop at the universal cover.
As for sets, suppose you went with the definition: any function that takes in a rational number and spits out a boolean. So the Dedekind cut for
I expect that
could indeed be
(serpinski S)is also a set ifSis a set.