# System S5 - Universal Closure

## Notes

I'm not aware of this system being explicitly given a name in the literature, so I'm arbitrarily giving it the name S5-UC here. But, without giving it a name, there are a number of places that point out that it is not the same as S5 - JH

See, for example, Hughes and Creswell's "Modal Logic", the chapter on modality and existance, the comments in the Kripke semantics.) Specificly, see page 182, last paragraph.

Melvin Fitting's "First Order Modal Logic" [Fitting, 1998]covers the issue in better detail.

This system is weaker than S5, and any theorem of this system is a theorem of S5... But the converse is not true.

## Background

There is a tendency for people (particularly, for some reason, people dealing with computers people to want to assume that the axioms of S5 that are given by free variables such as:

```
Lp > p
```

are the same as the universal closure of those same axioms:

```
forall(p, Lp > p)
```

This is simply not the case.

The Barcan Formula:

```
L (forall(x, F(x)) > forall(x, L F(x))
is a valid theorem in S5, but is *NOT* a valid
theorem in the system you get when you universally quantify each axiom
of S5.

The Barcan formula for quantified Modal Logic was first introduced
by Ruth Barcan Marcus (publishing under her maiden name Ruth C.
Barcan) in 1946 [Ruth Barcan, 1946, "A Functional Calculus of First
Order Based on Strict Implication", Journal of Symbolic Logic,
Vol. 11, No. 1,  Mar., 1946), pp. 1-16] and later in her doctoral thesis.
The validity of it in universally quantified vs free variable
S5 is documented in the literature everywhere from
Melvin Fitting's "First Order Modal Logic" to numerious papers, to
standard textbooks like Hughes and Cresswell's "Introduction to Modal
Logic".
This issue is a problem for a number of Modal Logics, but for some
reason S5-UC standing in for S5 seems to be
the one most common miss-labeling.

Community
I'm unaware of any systematic analysis of which modal logic systems
are, or are not, changed by universal closure.  Papers in Modal
Logic, and text books in the field, avoid the problem by always using
the free variable forms consistantly.   If anyone knows of a systematic
study of which modal logics that universal closure change it would be
nice if they could forward a reference to me (John.Halleck@utah.edu).

Go to ...
Systems Page
Structures Page
Logic Page