Re: ​Mathematics with the potential infinite

[Vaughan Pratt]

>From /Oystein Linnebo's submission of Mon, 30 Jan 2023 09:19:06 +0100:

"we [with Stewart Shapiro] also define a translation from the non-modal
language of ordinary first-order arithmetic, based on translating "for all"
and "exists" as "necessarily for all" and "possibly exists", respectively."

Had Saul Kripke thought of that in his "Semantical Considerations on Modal
Logic", he might well have suggested, as the common binary relation for
A(x) and E(x), the equivalence relation relating all pairs of possible
worlds differing just in their value of x, with all other variables left
unchanged.  Had he done so, this would have been the first multimodal logic
with infinitely many modalities (assuming infinitely many variables).

To the best of my knowledge, this suggestion was first made in the abstract
of my FOCS'76 paper "Semantical Considerations on Floyd-Hoare Logic",
https://ieeexplore.ieee.org/document/4567894 , namely in the second half of
the sentence, "We give an appropriate axiom system which is complete for
loop-free programs and also puts conventional predicate calculus in a
different light by lumping quantifiers with non-logical assignments rather
than treating them as logical concepts."

The full paper, at http://boole.stanford.edu/pub/semcon.pdf , introduces
the concept in the paragraph on the second page following definition (2) ,
namely, "An immediate application is to the definition of modalities of the
form E(x) interpreted as the equivalence relation relating pairs of
interpretations differing only in their assignment to x."  This connection
is continued three paragraphs later with "In this light, another way of
viewing our interpretation of E(x) is as a program that
nondeterministically assigns an arbitrary element of D to x."

On page 4 (p.112 in the Proceedings) substitution is defined with
(S1)-(S3), with (S3) catering for E(x).  Three paragraphs further down, the
assignment statement X <-- RANDOM (in later work notated x := ?) makes its
first appearance.

Modal logic makes its first appearance on page 8 in section 3.2, with an
axiom system organized as Logical Axioms, Logical Inference Rules (namely
Modus Ponens and Necessitation), and Axioms for Basic Programs.  In
traditional (Hilbert-style) first order logic, axioms for quantifiers would
appear in the first two of these, with Generalization under Logical
Inference Rules along with Modus Ponens.  In our modal logic
axiomatization, quantifiers instead appear under Axioms for Basic Programs,
with random assignment axiomatized first.  As pointed out in the first
paragraph on page 9, "the reader familiar with predicate calculus will
recognize in the logical axioms and rules, together with the two
quantification axioms, a sound complete axiom system for the pure predicate
calculus, which we can regard as a language for talking about "assignment"
programs of the form X <-- RANDOM."  (Since the only programs at that point
are the random assignments, Necessitation P |- [a]P reduces to
Generalization, P |- A(x)P.)

I mention all this mainly because I'm not sure to what extent people have
even noticed, let alone absorbed, the idea of the equivalence relation of
random assignment as the appropriate possible-world semantics for
quantifiers viewed as modalities.  But for me personally it was also
helpful in reminding myself of which aspects of that idea were in that
particular paper.  After writing papers for half a century, one tends to
lose track of their details.

Incidentally I did submit that conference paper for peer-reviewed
publication. However the referee's report was highly negative.  However the
managing editor overrode the referee and accepted the paper.  However in
the meantime I'd agreed with the referee--not wanting to publish an
embarrassingly badly organized paper I started over from scratch,
eliminating the P{a}Q part while focusing on the modal logic part.

Inci-incidentally I believe that sort of overriding of overriding of ... is
called nonmonotonic logic, as in "I fell out of the plane, however I had a
parachute, however it did not open, however I landed in a haystack, however
I found the missing needle, ...".  Which as far as I know was first used in
print by Marvin Minsky.  Somewhere in the middle of the 1970s, Marvin had
popped across the eighth-floor AI playroom to my office at the AI-theory
border to ask whether the concept of an inference rule capable of
overriding other rules had a name.  I immediately said I'd never heard of
it but that a natural name for it would be nonmonotonic logic, and Marvin
went with that.  John McCarthy at Stanford had been calling it
circumscription but I'd never have come up with that name in a lifetime of
answering Marvin's questions about logic.

Vaughan Pratt
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20230131/4aa6b447/attachment-0001.html>