First-order Logic is a Modal Logic

A modal logic is one that has a symbol with “type” Prop → Prop. Sometimes this symbol is written as a square, but I find this to be a pretty bizarre convention. It's important to add that modal logic is a framework. There aren't agreed-upon axioms of modal logic, nor an agreed-upon meaning to that symbol. It's just a piece of syntax we can sometimes assign useful meaning to.

Modal logic is a way to reason about the many ways a statement can be true. For example, a statement might be true, or it might just be believed by Sue (but not true). So one mode in which a statement can be true is “believed by Sue”. It's often useful to internalize this mode of truth, in which case it would be an operator on statements; we would write, say, Sue X to mean that Sue believes X, which itself would be a statement that might be true or false. You then add axioms that restrict what Sue believes, so we can reason about her beliefs. You might think of these axioms as tying the “real truth” and “believed by Sue” modes of truth together.

Modal logics are modeled (normally¹ [¹ As in, modal logics that can be modeled like this are called “normal”.]) by a set of “possible worlds” and also a “accessibility relation” between them. What people call the “possible worlds” is better thought of as the set of possible contexts. For example, if you've got some variables, there's a possible world for every instantiation of those variables. These possible worlds exist even if you're not doing modal logic: classical logic is modeled by a boolean algebra because a statement like x is true in some worlds but not others. It's the accessibility relation that defines the modal logic, and axioms of modal logic are just properties of this relation.

The meaning of the modal symbol, like Sue, is that Sue α is true in any worlds where α is true in any accessible worlds. So the modal symbol connects different possible worlds together.

Consider the statement x is prime. Is it true?

It is true when x is 2, 3, or some other prime, of course, and zero otherwise. That is, x is prime is a statement which has truth values in a collection of possible worlds.

Now consider ∀x, x is prime. This too is a statement!

In fact, ∀x is a symbol that transforms statements into statements, so it seems to fit the bill to be a modality. Think of it as internalizing the mode of truth that looks at x is prime and asks, “is that true for all x?”

Two worlds are ∀x-connected if their values of any constant except x are the same. This relation models the ∀x modality.

For example, let's say x ranges over booleans. There are two possible worlds: x is either true or false. A statement like x or x ∨ ¬ x is true or not true at each world. For example, x is true at only one of the worlds, while x ∨ ¬ x is true at both. Now, since the two worlds differ only in their value for x, they are ∀x-related. So ∀x, x is not true at either world: even in the world where x is true, the one where it's false is accessible. Meanwhile ∀x, x ∨ ¬ x is true at both worlds, because from both worlds it's true in all accessible worlds.

The universal quantifier is defined by its elimination and introduction principles.

Elimination: if you know ∀ x, α[x], where α[x] is some formula with x free, then you can conclude α[s], where s is any of the concrete values that x ranges over.

Introduction: if you can prove α[x] without knowing anything about x, then you have a proof of ∀x, α[x].

Let's look at introduction, first. This isn't an axiom—it's a rule. After all, just because x is prime, we don't necessarily know that ∀x, x is prime. The first might be true (in some contexts), while the second is definitely false. So this introduction principle isn't the axiom α → ∀x, α. Instead, it is the rule “if α, then ∀x, α.”

All normal modal logics have a rule just like this, called the N rule: “if α, then ◻α.” The proof is, if a statement is true in all worlds, then it's definitely true in all accessible worlds. The introduction rule for universal quantification is just one instance of the N rule.

The elimination rule is trickier. It is clearly true in our model, so we can admit it as an axiom governing the behavior of ∀x.

Also note that it has some implications that are easier to analyze from a modal-logic point of view. For example, it guarantees that ∀x, α → α. This is a modal axiom sometimes called T, and it corresponds to a reflexive relation. That's good, because the ∀x relation we defined is reflexive! It's also true that (∀x, α) ∧ (∀x, α → β) → ∀x, β. This is a modal axiom called K, and it's true for all normal modal logics.

Our relation is transitive, so the 4 axiom ought to hold: ∀x, α → ∀x ∀x, α. This axiom is confusing to understand, but translated into our model it tells us that if we change x and α stays true, then we change x twice and α will still stay true. That seems true.

We can define (classically) ∃x as ¬∀x¬, so we can also talk about axioms like (∀x, α) → (∃x, α), which is true when our relation is “endless”, which happens exactly when there is at least one value of x. We can also appreciate axioms like α → ∀x∃x, α, a bizarre axiom that tells us that our relation is symmetric.

You can think of first-order logic as a modal logic, and in fact first-order modal logic as just a multi-modal logic.