Propositions that can't be used to distinguish possible worlds

Are there known ways of formalizing the notion of propositions that can't be targeted by counterfactuals in a coherent way? Or of propositions that are outside the scope of the framework in question?

As a quick example of what I mean, here's an example of extending a modal logic (let's say S5 for concreteness) with a non-primitive modal operator `Y` that attempts to capture some of the intuition I'm going for.

Let's take a proposition like `The number 4 exists.`. There are many, many ways of analyzing that proposition including denying that it has a meaning or denying that it has a truth value. Let's suppose we're working in a framework that accepts that `The number 4 exists.` has a truth value, but doesn't commit to a particular truth value. Let's further suppose that our framework imposes the additional constraint that all possible worlds in our framework have the same truth value for `The number 4 exists.`.

In a certain sense, we've said something rather interesting about our notion of possibility/necessity, namely that it isn't powerful enough to consider questions like the existence of numbers but doesn't make a commitment either. Another way of looking at it is this is the "inside view" of questions outside the scope of the framework we're working in.

I can think of one sort of silly way to formalize this with a derived modal operator `Y` which means

``````Yx = ALxLNx     either x is necessarily true or x is necessarily false
``````

`Y` has some nice properties like closure under negation.

``````Yx  if and only if   YNx
``````

`Y` is also closed under conjunction.

``````Ya and Yb  implies  YKab
``````

And `{N,K}` is functionally complete, which is good but hardly definitive.

• Forster calls predicates that satisfy ∀x(P(x)↔□P(x)) noncontingent, and characterizes modal machinery (accessibility relations; relations of satisfaction between propositions and worlds; relations of habitation between objects and worlds; relations of correspondence or identity across worlds; the property of being a possible world) as noncontingent, see Modal Aether. Of course, the identity predicate is famously noncontingent, according to Kripke. Dec 21 '18 at 2:42
• @Conifold, the identity predicate is binary. Are we / is Kripke quantifying over the left and right possible world independently or together? Dec 21 '18 at 6:16
• P can be a multi-place predicate, x is meant to be a tuple of variables, and ∀ quantifies over each. See necessity of identity for Kripke's arguments. Dec 21 '18 at 18:52