/sci/ - Science & Math

>>15180515
Another interesting alley is to drop excluded middle, since then the concept of "function" is a much more restrictive one.
E.g. Peano arithmetic PA proves that every program either halts or does not halt, which makes "halts: (N^N)->{yes, no}" a functional association. Meanwhile, in the metalogic we find that there's actually no computable function for which PA would prove that it decides the halting problem, so the above "function" is not of the computable kind (a bit like how Choice postulates there's functions that we however know not to be of the computable kind). In turn, constructively you can postulate that the function spaces like N->{0,1} a.k.a. 2^N only hold computable functions, and this object then becomes "much smaller" than the elusive P(N) and you can postulate it to exist without needing to postulate powerset.
The constructive set theories like that are nice and they are close to type theory: You can postulate that Y^X exists even for countably infinite sets Y^X, while also postulating that Y^X is not bigger than N, in the sense that a subset I_{X^Y} of N surjects onto Y^X. E.g. you can list all the computable functions from N->N, which can be taken to equal N->N. And so indeed, you can here postulate that all sets A in this theory correspond to some index set I_A of S.
Although without excluded middle you have to rethink both the meaning of "function" as well as that of "subset". This theory however has no Dedekind reals and the Cauchy reals a priori have no modulus of convergence. The index sets I will be subsets of N, but they aren't countable (because for something to be countable you'd need to be able to actually count them (programmatically), which is not something classical ZF ever requires.)
Finally, if you further give up on excluded middle and countable choice, you can turn something like Dedekind reals countable.