# What are the axioms for quantified modal logic?

The plainest vanilla variety of propositional modal logic introduces two operators <> which is possibility, and [] which is neccessity. The axioms are:

p iff ¬□¬p

p iff ¬◊¬p

What is the simplest modification of this scheme when introducing quantifiers? ie All(∀) and Exists(∃)?

The SEP suggests that for SQML that one introduces the axiom:

x p(x) iff ¬∀x ¬p(x)

which seems eminently reasonable - as it says that there is an x that satisfies p iff it isn't the case that there is no x that doesn't satisfy p.

But are there any natural axioms that involve the quantifiers with the modal operators?

• Have you come across the "Simplest Quantified Modal Logic"? (SEP has a relevant entry that seems to work through axioms) Commented Oct 10, 2014 at 23:13
• Only in the vaguest possible terms - its referenced in my question ;). Commented Oct 11, 2014 at 0:38

I'm not an expert on modal logic, so take my answer with a grain of salt. I don't recall reading any discussion of a formal system where a quantified modal formula was an axiom of the system. (There may be some that I haven't come across, of course.) The point of adding quantification, and other devices that belong to first-order modal logical such as the property abstraction operator, is to increase the expressive power of the modal logic in order to use modal logic to formalize a broader range of natural language arguments that turn upon possibility and necessity.

Consider, for instance, the following "argument":

1. Necessarily, the President of the United States is the President of the United States.
2. Barack Obama is the President of the United States.
3. Therefore, necessarily Barack Obama is the President of the United States.

3 would appear to follow from 1 and 2 by a substitution rule. But this is surely incorrect. It turns out that the problem is a kind of ambiguity in (1). It appears that we need a way to distinguish two different ways to ascribe modal properties, we need to distinguish, in other words:

1*. It is necessarily true of the President, that he is the President.

from

1**. It is true of the President, that he is necessarily President.

1* is a harmless conceptual truth, but 1** is a patent falsehood. But (3) would only follow only from 1** and 2, not from 1* and 2. So clearly, in order to avoid making fallacious modal arguments we are going to have to have some formal machinery to distinguish between cases like 1* and 1**.

Notice now that there isn't really any way to do this using just propositional modal logic. We're going to need some quantifiers, and we're going to need "property abstraction", which is the modal analogue to the definite descriptor in ordinary first-order logic. (For more details, I would recommend looking at the very nice exposition of this in the relevant chapter of Fitting and Mendelsohn's First-Order Modal Logic textbook.) In other words, the addition of the machinery isn't so much just to create new logical systems, but to give us the needed expressive power to avoid some paradoxes.

• I guess what I'm saying is: the motivation for introducing the first-order machinery isn't quite the same as the motivation that typically underlies introducing new axioms in propositional modal systems, where the goal is to see what new theorems you get with your cool new axiom. The motivation is rather to avoid problems like the one that I mention above. At least, that's my impression. Maybe some of the other folks will know better.
– user5172
Commented Aug 23, 2014 at 19:02
• Is it worth noting that possible world semantics shows that modal operators quantify over worlds? I haven't come across the property abstraction operator, does this somehow turn a proposition into a predicate? Commented Oct 11, 2014 at 0:30
• Technically it terms a sentence into a term. "Lambda.x<Phi(x)>" is the abstraction of the sentence "Phi(x)," so you read it as "x's phi-ness."
– user5172
Commented Oct 11, 2014 at 10:54