[FOM] S4 + ZFC

[Allen Hazen]

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