Can’t you define C⊢SX for any set C of partitions of X, rather than C⊢FX w.r.t. a specific factorization F, simply as C⊢SX iff ⋁S(C)≥SX? If so, it would seem to me to be clearer to define ⊢ that way (i.e. make 7 rather than 2 from proposition 10 the definition), and then basically proposition 10 says “if C is a subset of factors of a partition then here are a set of equivalent definitions in terms of chimera”. Also I would guess that proposition 11 is still true for ⊢S rather than just for ⊢F, though I haven’t checked that 11.6 would still work, but it seems like it should.
Can’t you define C⊢SX for any set C of partitions of X, rather than C⊢FX w.r.t. a specific factorization F, simply as C⊢SX iff ⋁S(C)≥SX? If so, it would seem to me to be clearer to define ⊢ that way (i.e. make 7 rather than 2 from proposition 10 the definition), and then basically proposition 10 says “if C is a subset of factors of a partition then here are a set of equivalent definitions in terms of chimera”. Also I would guess that proposition 11 is still true for ⊢S rather than just for ⊢F, though I haven’t checked that 11.6 would still work, but it seems like it should.
I could do that. I think it wouldn’t be useful, and wouldn’t generalize to sub partitions.