Semantical Investigations on Non-classical Logics with Recovery Operators: Negation

We investigate mathematical structures that provide a natural semantics for families of (quantified) non-classical logics featuring special unary connectives, called recovery operators, that allow us to 'recover' the properties of classical logic in a controlled fashion. These structures are called topological Boolean algebras. They are Boolean algebras extended with additional unary operations, called operators, such that they satisfy particular conditions of a topological nature. In the present work we focus on the paradigmatic case of negation. We show 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, which feature recovery operators used to earmark propositions that behave 'classically' in interaction with non-classical negations. In contrast to traditional semantical investigations, 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 become encoded as algebras of sets via their Stone-type representation. We employ our higher-order meta-logic to define and interrelate several transformations on unary set operations (operators), which naturally give rise to a topological cube of opposition. Furthermore, our approach allows for a uniform characterization of propositional, first-order and higher-order quantification (also restricted to constant and varying domains). With this work we want to make a case for the utilization of automated theorem proving technology for doing computer-supported research in non-classical logics. All presented results have been formally verified (and in many cases obtained) using the Isabelle/HOL proof assistant.