Establishing validity of ◊(∃x)◻[(E!x ⊃ Ox) & E!x]/ ∴ (∃x)◻[(E!x ⊃ Ox) & E!x]

Question

I was wondering under which sort of quantified modal logic S5 system would the inference from ◊(∃x)◻[(E!x ⊃ Ox) & E!x] to (∃x)◻[(E!x ⊃ Ox) & E!x] be valid. Would this require a constant domain S5 system or can this be done in a variable domain S5 system? I know this works in a constant domain S5 system (with the Barcan formula) since one can use the Barcan formula to make this inference (by moving the possibility operator on the outside to the inside just before the necessity operator -- which the Barcan formula allows -- and to then eliminate the possibility operator using S5 leaving just the necessity operator, which results in (∃x)◻[(E!x ⊃ Ox) & E!x]). However, I was wondering if this can be done in a variable domain S5 system that does not involve the Barcan formula or the like.

Thank you.

Answer 1

I'm kind of assuming that by "E!x", you mean "x exists in the world under consideration".

It sounds like you basically want to go from ◊(∃x)◻ to (∃x)◻.

This is valid in S5, without Barcan formula and without assuming constant domains.

Indeed, if ◊(∃x)◻P holds in a world u then there is some world w where there is an individual x such that in all worlds v, x has property P. In particular, x exists in u (if this is required in order to have a property; or by your E!x formula, otherwise). So (∃x)◻P holds in u.