Is there an algebrization of second-order logic, analogous to Boolean algebras for propositional logic and cylindric and polyadic algebras for first-order logic?
[Math] Algebrization of second-order logic
higher-order-logicslo.logic
Related Solutions
This is a long list of questions! These are all related to a certain extent, but you might consider breaking it up into separate questions next time.
Proof theorists tend to prefer systems with many rules and few axioms such as natural deduction systems and Gentzen systems. The reason is that these are much easier to manipulate and visualize. (Look at the statement and proof of the Cut Elimination Theorem for an illustrative example.) Model theorists tend to prefer lots of axioms and just modus ponens, like Hilbert systems. The reason is that the semantics of such systems are easy to handle, and semantics is what model theorists really care about.
The real difference between propositional and first-order logic is quantification. Quantifiers are naturally more expressive than logical connectives.
There are many, many flavors of higher-order logic. The two main classifications are set-based systems and function-based systems. There are variants which don't really fit this division and there are variants which mix both. With strong enough internal combinatorics, these are all equivalent.
The set-based system have a set A of type 0 objects, which are considered atomic. Type 1 objects are elements of the powersets ℘(An). When the base theory has an internal pairing function (like arithmetic and set theory), the exponent n can be dropped. Then, type 2 objects are elements of the second powerset ℘(℘(A)), and similarly for higher types. Set-based higher types are somewhat inconvenient without an internal pairing function.
Function-based systems are similar, with functions An→A as type 1. Again, with an internal pairing function, the higher types streamline to A → A, (A → A) → A, ((A → A) → A) → A, etc. However, it is common to use more complex types in these systems.
Be careful how you read Gödel's Incompleteness Theorem. For first-order logic, the hypotheses state that the theory in question must be recusively enumerable and that it must be powerful enough to interpret a reasonable amount of arithmetic. Those are important hypotheses. (And they explain why no such theorem exists for propositional logic.) There are many variants for higher-order systems, but you need to be even more careful when stating them.
You can appreciate the difference between the different levels of higher-order logic by reading about Gödel's Speed-Up Theorems.
Most of mathematics today is based on set theory, at least in a theoretical sense. In set theory, higher types are interpreted internally using powersets and sets of functions. They also extend transfinitely and this transfinite hierarchy of higher types was shown necessary to prove theorems very low in the hierarchy, such as Martin's Borel Determinacy Theorem.
You may want to read on categorical logic.
The following is due to Magidor:
Theorem 1. Is $\kappa$ is a strong cardinal, then $LS(L^2) < \kappa.$
The proof if easy. Let $T \subseteq L^2$ be a theory and let $A$ be a model for $T$. e may assume the universe is some cardinal $\delta.$ Take some cardinal $\beta > \beth_{\omega}(\delta)$, and let $j: V \to M$ witness $\kappa$ is $\beta$-strong. It is easily seen $M\models$``$A \models T$'', so $M \models \exists B( B \models T, |B| < j(\kappa))$. By elementarity in $V$, $T$ has a model of size $< \kappa.$
Also note that for any theory $T \subseteq L^2,$ there is a least $\delta_T$ such that if $T$ has a model, then it has a model of size $< \delta_T.$ Then $LS(L^2)=\sup \{\delta_T: T$ as above $\}$, so $LS(T^2)$ can be singular, even though it can be above some very large cardinals.
Best Answer
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.