theHigherGeometerIs is possible to pin down a characterisation of definable functions between ordinals in ZFC?
EDIT: oh, wait, I meant *constructible*!
Since the product of two von Neumann ordinals a and b is well-ordered, there is a von Neumann ordinal axb of this order type. One might really hope that the two functions axb -> a and axb -> b are constructible.
And whenever one has constructible functions c -> a and c -> b, then the resulting c -> axb is constructible. So then you can talk about the finite product structure on Ord (one needs the unique function a -> {ø} to be constructible as well, but this should be ok!).
Then if one can define the 'constructible power set' Def(a) of an ordinal a, you can look at those constructible subsets of axb that are the graphs of functions. I'm not sure if this latter definition needs care (as in, does one need to be able to write what it means to be a function in some constructible way?)
These notes (on the constructible universe) by @AndresCaicedo are really good
https://caicedoteaching.wordpress.com/wp-content/uploads/2009/12/502-l.pdf
and probably cover a lot of what I'd want (I see there the definition of the well-ordering of \(L_{\alpha+1}\) from the well-ordering on \(L_\alpha\), which should generalise to defining a well-ordering on \(\mathrm{Def}(\alpha)\) from the well-ordering on \(\alpha\). if this works out, then the ordinal isomorphic to the order type of \(\mathrm{Def}(\alpha)\) might play the role of the power object \(P(\alpha)\) in my putative topos version of \(L\), with only ordinals as objects.
Further, I think that it might just be possible that since von Neumann ordinals are transitive, a first-order formula in the language of set theory with parameters from a given ordinal, might well be more-or-less equivalent to a first-order formula in the language of a (well-)ordered set. In this case, you really only need to know about the underlying well-ordering, not the full \(\in\)-relation on the tree the ZF-set gives.
Well, my idea is very very shaky: the powerset of an infinite ordinal \(\alpha\) in L is only completed a long time later, much much further up the constructible hierarchy, and certainly not just at the next stage! 😞
CubeRootOfTrue@highergeometer I like using non-binary logic. So 0.00100101b10101 ... is a real number, where b is both 0 and 1. It's the third truth value that solves the Liar Paradox #RM3 and other relevance fallacies. Cantor proved this. You can make a list of the reals, but some of the diagonal elements are unknowable, they are both 0 and 1. Like the Liar. #dialetheism
@CubeRootOfTrue I don't know enough about dialethism to give an informed response. But I do know that the diagonal argument isn't really a relevance issue, since you don't use weakening (or even symmetry), only contraction.
It may well be that in dialethic logic you get that the reals are both countable and uncountable, from positing the existence of such a real number as you have. However, I point out that the diagonal argument doesn't literally need to use the diagonal, so I suspect you can route around digits with more than one value, unless you radically redefine what you mean by real number.
That said, the diagonal argument really isn't about binary or decimal or ... expansions of real numbers. If you are dealing with those, you already have to worry about non-unique representations, about what you mean by real numbers (Dedekind cuts, equiv classes of Cauchy sequences etc) and worry whether these even have the properties you want them to have. Throwing in more real numbers where digits in some binary expansion have multiple values like you propose doesn't remove all the other binary expansions that have definite values. If the smaller set of real numbers with dialethic-ignoring binary expansions is not countable, then the larger set with these exotic real numbers can't be countable.
@CubeRootOfTrue If you read https://doi.org/10.32408/compositionality-5-8 and have ideas about what happens in dialethic logic then go for it. I'm thinking that the assumption in Theorem 11 that there is a t-free endomorphism might be the weak point, but as I said, I don't know enough about dialethism to be confident about claiming anything.
