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.
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.