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