>>12942841I don't know why you bring time into it, but essentially this seems correct.
N is a set by Infinity (axiom) and one in which membership is decidable. So the class
X := {5,8,9, 6887}
is a subset of N by Separation (axiom) too, and thus a set (as opposed to a proper class).
The class
S := {x | (x=8 or x=6887) and ((x is prime) or (x is not prime))}
is a subset of X by Separation again, and thus also a set.
Classically S equals {8, 6887} by LEM (axiom), i.e. S={8, 6887}
Constructively, it also equals {8, 6887}! But the proof of that needs more work: You need to find out whether 6887 is prime or not prime while proving S={8, 6887}.
Moving on, to elaborate: For any predicate, the class {x in X| P(x)} is a set by Separation.
So the power of the singleton set X={7} is as rich as the truth values of your theory. Apriori, this class
?={s | s is a subset of {7}}
is proper.
If you adopt the Powerset axiom (all powerclasses are sets), then ? also a set.
If you adopt LEM, then by this act ? comes to be in bijection with the function space
{7}->{true, false}, which is in bijection with just {true, false}.
You may adopt the axiom that all function spaces X->Y are sets whenever X and Y are. This is weaker than the Powerset axiom and is often done, because it's natural from a type construction perspective (see e.g. typed lambda calculus). But that just essentially means that all subsets given rise to by decidable predicates are sets.
>>12943449>The classifier was extremely approachable in this case. Nice one.There's a book fleshing out the sheave topoi for four (iirc) such discrete structures in detail
https://www.researchgate.net/publication/333579691_Generic_figures_and_their_glueings_A_constructive_approach_to_functor_categoriesGood to get a graphical/finite intuition for some of the objects involved
>>12943345Accepting LEM just kills off meaningful interpretations, that's why I think it's inevitable to have a logic around that doesn't adopt it.
