2022/05/21 by W. Dzik, Dzik, W., S. Kost +3
Computer Science · Mathematics · #03B45 #03B55 #06D20 #06E25 #68T27 #Advanced Algebra and Logic #Advanced Topics in Algebra #FOS: Mathematics #Logic (math.LO) #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2205.10644
openalex publication_date 2022/05/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Following a characterization [10] of locally tabular logics with finitary (or unitary) unification by their Kripke models we determine the unification types of some intermediate logics (extensions of \sf INT). There are exactly four maximal logics with nullary unification \mathsf L(\mathfrak R2+), \mathsf L(\mathfrak R2)∩\mathsf L(\mathfrak F2), \mathsf L(\mathfrak G3) and \mathsf L(\mathfrak G3+) and they are tabular. There are only two minimal logics with hereditary finitary unification: \mathsf L(\mathbf Fun), the least logic with hereditary unitary unification, and \mathsf L( \mathbf Fpr) the least logic with hereditary projective approximation; they are locally tabular. Unitary and non-projective logics need additional variables for mgu's of some unifiable formulas, and unitary logics with projective approximation are exactly projective. None of locally tabular intermediate logics has infinitary unification. Logics with finitary, but not hereditary finitary, unification are rare and scattered among the majority of those with nullary unification, see the example of \mathsf H3\mathsf B2 and its extensions.