Mathematics with the potential infinite

[Vaughan Pratt]

Thanks, James.

"I think there is significant room for diversity in what counts as a
(finite description of a) procedure for a finitist / potentialist."

I believe I had a similar thought back in 1980 regarding the principle
of induction and the meaning of Kleene star as the defining operation
of Kleene algebras.

In 1979 Dexter Kozen and I had essentially independently come up with
the idea of a dynamic algebra as a Boolean algebra equipped with
infinitely many operators in the sense of Tarski and Jonsson back in
1951.

The difference was how Dexter and I defined Kleene star in dynamic
logic, namely <a*>P, for any given action a and proposition P.

Dexter defined <a*>P as an infinite disjunction P v <a>P v <a><a>P v
... while I defined it via the equation <a∗>p <= p ∨ <a∗>(p′ ∧ <a>p).
(x <= y is the equation x v y = y.)  My equation is simply how to
express induction in that particular language.  A little later Fran
Berman pointed out that only my definition was compact.

Dexter was so convinced I'd stolen the idea of a dynamic algebra from
him that the book on dynamic logic that he cowrote a decade later with
my friend Jurek Tiuryn and my first Ph.D.student David Harel,
currently the president of the Israel Academy, declined to credit me
with the invention of dynamic logic, instead attributing it to earlier
writers.  This was despite the fact that none of those earlier writers
had made any connection whatsoever with Kripke structures, the reason
I titled my paper "Semantical Considerations on Floyd-Hoare logic".

In summary, there are no papers by me on dynamic algebras where I have
not credited Dexter as the inventor of the concept, despite the fact
that Dexter's invention involves absolute infinities while mine only
involves the potential infinities of induction.

Which raises the following questions.

1.  Given all that, can you nevertheless argue that Dexter was
justified in his removal of me from his book on dynamic logic as its
inventor?

2.  Is the free group on one generator potentially or actually infinite?

3.  Does compactness bear on these questions?

Vaughan