We investigate mathematical structures that provide natural semantics for families of (quantified) non-classical logics featuring special unary connectives, known as recovery operators, that allow us to 'recover' the properties of classical logic in a controlled manner. These structures are known as topological Boolean algebras, which are Boolean algebras extended with additional operations subject to specific conditions of a topological nature. In this study we focus on the paradigmatic case of negation. We demonstrate how these algebras are well-suited to provide a semantics for some families of paraconsistent Logics of Formal Inconsistency and paracomplete Logics of Formal Undeterminedness. These logics feature recovery operators used to earmark propositions that behave 'classically' when interacting with non-classical negations. Unlike traditional semantical investigations, which are carried out in natural language (extended with mathematical shorthand), our formal meta-language is a system of higher-order logic (HOL) for which automated reasoning tools exist. In our approach, topological Boolean algebras are encoded as algebras of sets via their Stone-type representation. We use our higher-order meta-logic to define and interrelate several transformations on unary set operations, which naturally give rise to a topological cube of opposition. Additionally, our approach enables a uniform characterization of propositional, first-order, and higher-order quantification, including restrictions to constant and varying domains. With this work, we aim to make a case for the utilization of automated theorem proving technology for conducting computer-supported research in non-classical logics. All the results presented in this paper have been formally verified, and in many cases obtained, using the Isabelle/HOL proof assistant.

翻译：本文研究为一系列具有特殊一元联结词（称为恢复算子）的（量化）非经典逻辑家族提供自然语义的数学结构，这些恢复算子允许我们以受控方式“恢复”经典逻辑的性质。这些结构被称为拓扑布尔代数，即通过附加拓扑性质约束的运算扩展的布尔代数。本研究聚焦于否定的范式情形，论证这类代数如何为若干家族的子一致形式不一致逻辑和子完全形式未定逻辑提供语义。这些逻辑包含恢复算子，用于标记与非经典否定交互时表现为“经典”的命题。与以自然语言（辅以数学简写）进行的传统语义研究不同，我们的形式元语言采用高阶逻辑（HOL）系统，且存在对应的自动化推理工具。通过斯通型表示，我们将拓扑布尔代数编码为集合代数，并运用高阶元逻辑定义并关联一元集合运算的若干变换，由此自然形成拓扑对立立方体。此外，该方法能统一刻画命题、一阶和高阶量化（包括常域与变域约束）。本研究旨在论证利用自动定理证明技术开展非经典逻辑计算机辅助研究的可行性。论文所有结果均已通过Isabelle/HOL证明助手进行形式验证，其中多数结果亦由其自动推导得出。