What kind of system results if you add quantifiers over truth values / truth-valued variables to classical sentential logic?
Does the kind of system that results have a name?
Is there a straightforward translation from classical sentenial logic + truth value quantifiers into a more well-known/common system that doesn't result in exponential blowup of the terms? (i.e. ruling out $Πc\varphi \mapsto \left(\varphi[c:=\bot] \; \land \; \varphi[c:=\top] \right)$ and $Σc\varphi \mapsto \left(\varphi[c:=\bot] \; \lor \; \varphi[c:=\top]\right)$) I'm assuming that, if such a translation exists, then classical logic + truth value quantifiers might be just a curiosity or a nonstandard notation for a subset of an existing thing.
The Wikipedia article on Polish notation gives two quantifiers Σ and Π, corresponding to the more familiar $\exists$ and $\forall$, respectively.
Here's an excerpt from the table explaining the mapping between conventional and Polish notation, $p$ is intended to range over variables and $\varphi$ is an arbitrary wff.
\begin{array}{|c|c|c|} \hline \text{Operator} & \text{Polish Notation} & \text{Conventional Notation} \\ \hline \text{Universal quantifier} & Πp\varphi & \forall p . \varphi \\ \text{Existential quantifier} & Σp\varphi & \exists p . \varphi \\ \hline \end{array}
Since Łukasiewicz's notation is a notation for sentential logic which, traditionally, has no notion of individuals in a domain of discourse to be quantified over, the table helpfully has an explanation of what the quantifiers mean.
Note that the quantifiers ranged over propositional values in Łukasiewicz's work on many-valued logics.
This almost immediately strikes me as a generalization of tautology / satisfiability. Normally an expression like $P \land Q$ stands on its own and whether it's supposed to be a tautology or supposed to be satisfiable isn't surfaced in the notation and doesn't seem to be part of the intrinsic meaning of the expression.
However, Σ and Π can trivially be used to surface whether we want to consider the consider the resulting expression as a tautology or potentially satisfiable thing just by adding a prefix of $ΣaΣbΣc\cdots$ or $ΠaΠbΠc$ to bind the free variables in the matrix of the expression.
It's more general than just that, since $(Σa(a \land a)) \lor (ΠaΠb(a \lor b))$ is expressible.
In the appendix to his Formal Logic A. N. Prior calls systems with an implication connective and a universal quantifier over propositions, "Extended Propositional Calculus".