# [FOM] S4 + ZFC

Allen Hazen allenph at unimelb.edu.au
Fri Aug 24 03:41:05 EDT 2007

```Mike Carroll asks about the history of combining
set theory with S4 modal logic.  There is a bit
of a history.

S4 has often been proposed as the logic of
(idealized: not what we REALLY know, but what we
could IN PRINCIPLE figure out) knowledge:
interpret the square as meaning "It is known
that" or "person x knows that."  This idea dates
at least from Hintikka's "Knowledge and Belief"
(pub. in early 1960s), one of the founding
documents of epistemic logic.  Provability is an
epistemic concept (proofs are supposed to yield
mathematical knowledge), and it is plausible (if
you ignore the complications produced by Gödel's
incompleteness theorem and Löb's theorem) that S4
is the right logic of "it is in principle
provable that."  (For the proper axiom of S4, "if
it is necessary that P, then it is necessary that
it is necessary that P": well, if P is provable,
then there is a proof of it, and by presenting
the proof you will have proved that there is a
proof of it!)  This idea struck Gödel in the
1930s: his "Interpretation of intuitionistic
propositional logic" (item 1933f in volume I of
Gödel's "Collected Works") gives the first
presentation of the modern axiomatization of S4
(with the square written B, for "beweisbar"),
claims the interpretation of intuitionistic logic
in S4, and ends with the comment that if you mean
"provable in a particular formal system" things
are more complicated.

Around 1980, the idea was taken up by Nicholas D.
Goodman: cf. his "The knowing mathematician," in
"Synthese," vol. 60 (1984), pp. 21-38.  He argued
that mathematics needed to be enriched by
incorporating the concept of mathematical
knowability into its content, and proposed that
"epistemic mathematics" (=mathematics as
formalized, not in plain classical logic but, in
quantified S4 with the square interpreted
epistemically) would allow classical
mathematicians to formulate and make use of some
of the distinctions familiar in constructive
mathematics.  This generated some excitement at
the time: a collection of papers, "Intensional
Mathematics," ed. Stewart Shapiro (Amsterdam:
Elsevier-North Holland, 1985) was published,
including a paper by Goodman entitled "A
genuinely intensional set theory."  Some further
work of a metamathematical nature was done: cf.
JSL papers by Goodman, Flagg and Scedrov (look in
the cumulative index in vol. 55 (1990)).
Mathematical theories in S4 and mathematical
theories in intuitionistic logic turned out to be
closely comparable.

There has been some other work on modal set
theory.  Smullyan and Fitting's use of S4 to make
Cohen's idea of forcing perspicuous is perhaps to
some degree anticipated by Daniel Gallin's use,
in his "Intensional and Higher-Order Modal Logic"
(North-Holland, 1976) of S5 in giving perspicuous
formulations of independence results (in type
theory) by Boolean-valued models.  Aldo Bressan's
"A General Interpreted Modal Calculus" (Yale
University Press, 1972) proposed a modal (S5)
version of simple type theory as a framework for
some axiomatization problems in physics.  Kit
Fine described (and proved a few results about)
(S5) modal set theory in an article in "Nous,"
vol. 15 (1981), pp. 177-205.  Perhaps the most
interesting is Charles Parsons's attempt to give
a modal formulation of the idea that set theory
investigates an indefinitely extendABLE universe,
in the last chapter of his "Mathematics in
Philosophy" (Cornell U.P., 1983, re-issued a few
years ago in paperback: a great book even if you
ignore the last chapter!): for some applications
a slightly stronger modal logic than S4 (S4.2) is
nicer....

Many philosophers (and philosophical
mathematicians) have been attracted by the idea
of "potential" infinity, an idea that seems to
call out for modal formulation.  Some interesting
thoughts (but not a full formulation in the
context of modal logic) can be found in an
appendix to Abraham Robinson's "Formalism 64," in
Y. Barhillel, ed., "Logic, Methodology and
Philosophy of Science: proceedings of the 1964
conference" (North-Holland, 1965).  I discussed
Robinson, Shapiro and Goodman, funny modal
logics, etc., in a paper (with, alas, some
embarrassing mistakes and errors, though mostly--
I hope-- minor ones) in J.M. Dunn and A.K. Gupta,
eds., "Truth or Consequences: essays in honor of
Nuel Belnap" (Kluwer, 1990), pp. 177-196.

Allen Hazen
Philosophy Department
University of Melbourne

```