What differentiates FOM from other religions?

[Vaughan Pratt]

After this extended discussion of finitism, which seems to have been
initiated by my great-great-grand-advisor Thoralf Skolem when he identified
PRA as a suitably finitistic logic in reaction to Russell and Whitehead's
*Principia Mathematica*, I've come to the conclusion that FOM religions are
differentiated from other religions by being linearly ordered.

Beyond the countable ordinals, only cardinals seem to matter.  Within the
countable ordinals, we have omega^omega for PRA, epsilon_0 for PA, and the
Feferman-Schuette ordinal Gamma_0 as (arguably) the first impredicative
ordinal.

In this message I'd like to shift attention to the logic of regular
expressions, in which Kleene star is the only operation that can be
considered infinitary in any sense.

And since PRA can be organized as a purely equational theory (although its
extension to a Horn theory is also of interest), one can ask about
equational theories of regular expressions.  Here are three.

1.  Regular expressions as an equational theory.  These were studied in a
book titled Regular Algebra and Finite Machines by John Horton Conway,
where he confirmed V. Redko's proof that this theory had no finite
axiomatization.

2.  Propositional dynamic logic, PDL, the propositional fragment defined by
Mike Fischer and Richard Ladner of my first order dynamic logic, with
formulas of the form <a>p where a is a regular expression and p is a PDL
formula, closed under Boolean operations.  In ACM STOC'80 I gave a
Birkhoff-style algebraic proof of completeness of Krister Segerberg's
axiomatization of PDL.  Elsewhere I gave the first proof that that PDL was
decidable in exponential time.

3.  Action algebra <https://en.wikipedia.org/wiki/Action_algebra>, a
finitely axiomatizable equational theory conservatively extending 1 above
by introducing two residual operations, "p before a" and "p after a".

Common to all three is the ostensibly infinitary operation of Kleene star.

Although no numbers are mentioned, one imagines that a* is infinitary.  My
question is whether the infinitary nature of a* should be considered
potential or actual in each of these three logics of regular expressions.

Vaughan Pratt
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20230212/94a8a81e/attachment-0001.html>