How do we classify formal systems' (propositional logic, first-order logic, second-order logic, higher-order logic, Hoare logic and type theory) expressivity?
In the same way that grammars (CSG, CFG, ...), languages (CSL, tree-adjoining language, ...) and abstract machines (Turing machine, ...) 'fit' into the Type 0-3 range of the Chomsky hierarchy, can we also classify the formal systems into it?
Or, is there another yardstick for describing the relative expressive power of formal systems?
Comparison of logics is a complicated subject.
Expressive power of logics can be 'measured' in various ways. The most well-known approach is that of conservative extensions. If $L$ is a logic with signature $\Sigma$, then a logic $L'$ over signature $\Sigma' \supseteq \Sigma$ is a conservative extension of $L$ provided every $\Sigma$-formula $\phi$ that is provable in $L'$ is already provable in $L$. In other words, conservativity means that by moving from $L$ to $L'$ we are not adding expressive power to the discourse about things that can be expressed in $\Sigma$.
Things become more complicated when you are looking at logics with signatures that are not comparable by $\subseteq$. When you want to compare e.g. set theories with type theories, then you won't get a nice match of signatures. In this case you need to look at encodings. This can be done in various ways. For example you can encode formulae, or formulae an proofs. You can study properties of those encodings (e.g. do they preserve formula/proof structure) etc?
An old example of encoding is Gödel's and Gentzen's double-negation translation that embeds classical logic into intuitionistic logic, and reduces the consistency of the former to that of the latter.
Comparison of programming languages is even more complicated and -- kind of, sort of -- contains the comparison of logics as a special case by the Curry–Howard correspondence.
