Yiheng Wang

A sequent calculus S for the variety tqBa of all topological quasi-Boolean algebras is established. Using a construction of syntactic finite algebraic model, the finite model property of S is shown, and thus the decidability of S is obtained. We also introduce two non-distributive variants of topological quasi-Boolean algebras. For the variety TDM5 of all topological De Morgan lattices with the axiom 5, we establish a sequent calculus S5 and prove that the cut elimination holds for it. Consequently the decidability of S5 is established. Furthermore, this proof-theoretic method is applied to some subvarieties of TDM5.

In this paper, we consider the non-normal modal logics over monotonic modal logic M\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textsf{M}$$\end{document} with extensions of any combination of (N), (P), (T), and (4) i.e. {M,MN,…,MNPT4}\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\{\textsf{M},\textsf{MN},\ldots,\textsf{MNPT4}\}$$\end{document}. We study the algebras corresponding to these logics and give some examples of them. We further introduce the Gentzen-style sequent calculi with soundness and completeness proved. Finally, we prove the FMP of these logics and thus decidability based on our systems by algebraic proof-theoretic methods.