Is there an algebraization of second-order logic, analogous to Boolean algebras for propositional logic and cylindric and polyadic algebras for first-order logic?
3 Answers
Did programme of predicate calculus algebraization succeed? In his essay An autobiography of polyadic algebras Halmos outlined why he is not satisfied with his baby. I suggest that Cylindric algebras are not genuine algebras either; what other algebraic structures have operators parametrized by something (cylindrification)? The situation is strikingly different from either boolean or relation algebra, each having a set of intuitive binary, unary, [and 0-ary] operations.
I suggest that the culprit is positional perspective onto relation attributes. Positional perspective is ubiquitous in math (sequences, function arguments, etc), so is easy to see why it penetrated into the world of relations. Positional perspective makes perfect sense for binary relations, this is why nobody challenged its adequacy for n-ary ones. However, it is easy to see that attribute positions are not essential to the ability to match values of the two different attributes of two different relations. Named attribute perspective is widely used in database theory and practice, which implies yet another algebraization of predicate logic.
-
1$\begingroup$ Good point! It is also my impression that performing substitutions in predicate logic (cylindrical algebra) does not increase the length of formulas, whereas using relation algebra or $\lambda$-calculus would increase the length of formulas. Is that correct? $\endgroup$– YKYCommented Jan 21, 2017 at 0:43
-
$\begingroup$ Hyperdoctrines, invented by Lawvere, is a far more penetrating algebraization of predicate calculus. $\endgroup$ Commented Jul 5 at 15:36
-
$\begingroup$ What is your definition of a 'genuine algebra'? Modules and vector spaces also have operations parameterized by something (i.e., scalar multiplication), and for any fixed dimension $\alpha$, $\alpha$-dimensional cylindric algebras are algebras in the sense of universal algebra. $\endgroup$ Commented Jul 5 at 17:59
Have you looked at the following paper:
https://arxiv.org/abs/0807.4620
Christoph Koch: A Compositional Query Algebra for Second-Order Logic and Uncertain Databases
Very belatedly, I think it's worth noting that there is some work connecting higher-order logic and cylindric/etc. algebras, at least including the following: