A computational glimpse at the Leibniz and Frege hierarchies (Q1676326)

The author deals with the following problem: is it possible to decide whether the logic of a given finite consistent Hilbert calculus in a finite language belongs to a given level of the Leibniz or Frege hierarchy? In the first case, the Hilbert's tenth problem (on Diophantine equations) is reduced to the problem of classifying such a logic in the Leibniz hierarchy. In the second case, the author relies on the undecidability of the equational theory of relation algebras in a single variable. Thus, for both hierarchies the problem is generally undecidable. Moreover, the problem is shown to remain undecidable when restricted to the classification, within the Frege hierarchy, of finite consistent Hilbert calculi that determine a finitely algebraizable logic.