Intuitively, the more powerful a theory is, the greater the variety and quantity of ideas can be expressed through its formal language. Therefore, when comparing two theories concerning the same subject, it seems only reasonable to compare the expressive powers of their formal languages. On condition that the quantum mechanical description is universal and so can be applied to macroscopic systems, quantum theory is required to be more powerful than classical mechanics. This implies that the formal language of Hilbert space (...) theory must be more expressive than that of Zermelo-Fraenkel set theory. However, as shown in the paper, such a requirement cannot be met. As a result, classical and quantum formalisms cannot be in a hierarchical relation, that is, include one another. This fact puts in doubt the quantum-classical correspondence and undermines the reductionist approach to the physical world. (shrink)

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. (shrink)