# Can someone translate this into quantified modal logic?

So an attempt to translate- its not possible for two necessary beings to exist- in quantified modal logic. Is it correct?

¬◇∃x∃y[[□Nx ∧ □Ny] ∧ x ≠ y]

• Does the predicate N = necessity in predicate position? You might try moving the box operator in front of the existential operators, though: ¬◇[□∃x□∃y[x ≠ y]], although when I try to represent that in English, it sounds like saying that it's impossible for two beings to be necessarily distinct at all, which would be an odd conclusion. Commented Oct 11, 2023 at 17:13
• What does Nx mean? I assume it is somehow connect to "x exists necessarily" but I can't think of any obvious interpretation into (non-free) modal predicate logic. Commented Oct 11, 2023 at 17:27
• The necessity operator applies to propositions, not individuals. I think your first challenge is to find a way to represent "x exists necessarily" in terms of the modal necessity operator. Just saying something like □∃x(x=x) doesn't seem to work because it doesn't say anything about which x you are talking about. You could use predicates such as ∃F(□∃x(Fx)), but this requires second-order logic. Commented Oct 11, 2023 at 17:41
• @DavidGudeman hey David, thanks for response. Im actually learning and for this reason I asked if someone could translate it. Commented Oct 11, 2023 at 17:50
• If N is the predicate for 'necessary being', then I think you can simply drop the necessity operator and get the sentence you are looking for: ¬◇[∃x∃y[[Nx ∧ Ny] ∧ x ≠ y]] - It is not possible for there to exist some x and some y such that x is a necessary being and y is a necessary being while x and y are distinct. The necessity operator ([]) simply denotes necessity, whilst what you are attempting to denote using it is a necessary being, which dosen't work. You'll need a special predicate to denote that or some predicate that denotes 'being' to which you append a necessity operator. Commented Oct 11, 2023 at 18:27

The usual notion of necessity in Kripke semantics is different than the notion of necessity used by theists that posit necessary beings. However, there is a modality, usually denoted U(p), which means that proposition ‘p’ holds in all possible worlds as opposed to all accessible possible worlds. You can just define your ‘N’ operator as such a modality; in which case, you’d just want to remove the boxes from your formula and change N(x) to N(x=x) to achieve the desired translation. Since you’re using ◇, you’ll need two accessibility relations between worlds.

Given interpolation of necessity and impossibility (as "necessarily not"), let's drop the "not possible" symbolism for the moment:

• □∃xFx → (□∃yFy → □(x = y))

You'd have to gerrymander F well enough to absolutely guarantee uniqueness, then. Theological options would be F = mereological simplicity (consists of only one part), eternality (has a unique/disjoint relationship with time), etc. But then maybe you could tack on something like:

• a¬Fa(¬□∃aFa)

That is ambiguous between, "No a are such that Fa," and, "For all a that are such that not Fa," though.

Caveat: I am more proficient in natural-language argumentation than things like proof theory and programming. So the effect of things like Barcan formulae on the above presentation is something I'm unsure about. If your OP question is homework-related, see if you can double-check proposed answers, here, with a tutor at your school. Good luck!

Sidebar: sometimes we do use a uniqueness-indicating existential quantifier ∃!, so you might try out:

• □∃!xFx

Depending on whether you have iterations of modal operators be trivial or not, you might go on to:

• □□∃!xFx

To regain the diamond operator:

• ¬◊(¬∃!xFx)