[FOM] origins of completeness in modal logic

[Dana Scott]

On Mon, 2 Mar 2009 Max Weiss <30f0fn at gmail.com> wrote:

> For first-order logic, there is some intuitive notion of (classical)
> validity that is sufficiently stable to allow axiomatization and even
> the proof of a completeness theorem before the relevant semantical
> notions were completely formalized.  However, for modal logic this
> seems not clearly to be the case: the question of an arbitrary modal
> formula "is it valid?" tout court, seems simply ill-posed.
>
> But moreover, it is not just any mathematically precise method of
> "interpretation" that delivers a notion of validity nor hence of
> completeness.  Consider, for example, the result of McKinsey and
> Tarski (1944) that a formula is a theorem of S4 iff it is always
> assigned the top element in all closure algebras.  My impression is
> that this would not be considered a completeness theorem, since
> "always denotes the top element" is not an intuitively plausible
> notion of validity.  (For whatever reasons, the authors don't call it
> a completeness theorem.)
>
> Roughly speaking, what I'm wondering is what sort of basis there might
> be for considering, say, Kripke (1959), as opposed to such earlier
> work, indeed to contain "a completeness theorem in modal logic".  The
> motivation is not to try to establish relationships of historical
> priority, but rather to try to understand how the notion of
> completeness in modal logic arose in the first place.
>
> Perhaps understanding the development of the relevant notion of
> completeness would help to explain why Jonsson and Tarski don't, in
> their (1950), draw the retrospectively obvious connections to logic
> for their representation theorem.
>
> Any references, hypotheses, critical remarks, etc. would be much
> appreciated.

I think it is fair to say that Tarski & Co. were more interested in
Algebraic Logic than in completeness theorems.  Just as Boolean Algebra
is just a reformulation of Propositional Calculus  (one an equational
theory, the other an assertional theory).  So Closure Algebra is just
an equational form of Lewis' S4 Modal Logic, and Heyting Algebra is
just an equational form of Intuitionistic Propositional Calculus.
Equational theories have free algebras, and in finitary cases, the
free algebra on countably many generators satisfies EXACTLY the
equations provable in the theory.  Some, might call this a completeness
theorem, but it is a very lazy one.  The so-called Lindenbaum algebras
of the propositional calculi mentioned give free "interpretations"
(and free algebras); and saying "phi = 1" is just another way of
saying "phi is provable".

In the Boolean case, the two-element algebra can be considered
"canonical" -- especially when we take 0 as standing for False and
1 for True.  (Tarski actually liked it the other way around!)
So the question comes up: If an equation holds in the two-element
algebra, does it hold in the free algebra?  The well-known proof
uses homomorphisms to the two-element algebra.  The facts that only
finitary operations are used, and that a finitely generated Boolean
algebra is finite, make the existence of homomorphisms easy to
prove.  Another, more formal proof argues that if an equation is
not provable, then its adjunction to the axioms of Boolean algebra
allows a proof of the equation "x = y".

The other two logics are not so easy to deal with.  Is there a
canonical Heyting algebra or a canonical Lewis algebra?  I don't
think so.  Thus there is no way to argue that the axioms have
"completely captured" all the valid equations of a particular
"God-given" structure.  There may indeed be single structures that
do have just the equations of the theory, but we may not know of
them in advance of setting out the formal theory.  The Boolean
situation is very special.

In High-School Algebra we are very lucky indeed: The equations
in (+, x, -, 0, 1) true in the signed integers Z are exactly
the same as those true in the rationals, the reals, and the
complex numbers.  So one formal system of algebra does for all
these interpretations.  (We speak here of equations universally
valid, not whether certain equations have solutions.)  It was not
until we came to the quaternions that we had to review the rules
of algebra.  And finite fields need MORE equations.

With the logics mentioned it did turn out that equations true in
all finite Heyting algebras were generally valid, and the same for
Lewis algebras.  But as Godel showed, no finite model can be
canonical.  What to do?

Perhaps there is a canonical CLASS of models short of the class
of all models?  Maybe.  Maybe not.  Tarski (and many others) showed
that topological models suffice.  In the intuitionistic case,
using the the lattices of open subsets of topological spaces
suffices; in the modal case topological closure algebras suffice.
And there are even FIXED topological spaces that can be used.
This is not philosophically satisfactory, however, because the
the discovered models were not the primary motivation for the
study of the logics in the first place.

Kripke models (also discovered by Tarski & Co.) are specialized
topological spaces which also suffice, and the "possible worlds"
story makes them somewhat attractive philosophically. But where
do possible worlds come from and what governs choices of alternative
relations?  Things become even less clear (in the opinion of this
writer) when one moves on to predicate logic and the need to
interpret structures of individuals.  The topological models
work somewhat better for first- and higher-order logic, and
this has been studied in new detail since the discovery of
Topos Theory -- especially for intuitionistic logic.

In a completely different direction realizability and
"provability" interpretations of intuitionistic and modal
logics have more philosophical interest, but completeness
theorems are quite hard to formulate and work out.

I hope these opinions do not raise more questions than they
answer.

DANA S. SCOTT
University Professor, Emeritus
Carnegie Mellon University
Visiting Scholar in Logic and the Methodology of Science
University of California, Berkeley