In this paper, we develop the system LZF of set theory with the unrestricted comprehension in full linear logic and show that LZF is a conservative extension of ZF– i.e., the Zermelo-Fraenkel set theory without the axiom of regularity. We formulate LZF as a sequent calculus with abstraction terms and prove the partial cut-elimination theorem for it. The cut-elimination result ensures the subterm property for those formulas which contain only terms corresponding to sets in ZF–. This implies that LZF is (...) a conservative extension of ZF– and therefore the former is consistent relative to the latter. (shrink)

This brief article is intended to introduce the reader to the field of algebraic set theory, in which models of set theory of a new and fascinating kind are determined algebraically. The method is quite robust, applying to various classical, intuitionistic, and constructive set theories. Under this scheme some familiar set theoretic properties are related to algebraic ones, while others result from logical constraints. Conventional elementary set theories are complete with respect to algebraic models, which arise in a variety of (...) ways, including topologically, type-theoretically, and through variation. Many previous results from topos theory involving realizability, permutation, and sheaf models of set theory are subsumed, and the prospects for further such unification seem bright. (shrink)

In this paper we present a new categorical approach which attempts to provide an original understanding of QM. Our logos categorical approach attempts to consider the main features of the quantum formalism as the standpoint to develop a conceptual representation that explains what the theory is really talking about —rather than as problems that need to be bypassed in order to allow a restoration of a classical “common sense” understanding of what there is. In particular, we discuss a solution to (...) Kochen-Specker contextuality through the generalization of the meaning of global valuation. This idea has been already addressed by the so called topos approach to QM —originally proposed by Isham, Butterfiled and D ̈oring— in terms of sieve-valued valuations. The logos approach to QM presents a different solution in terms of the notion of intensive valuation. This new solution stresses an ontological reading of the quantum formalism and the need to restore an objective conceptual representation and understanding of quantum physical reality. (shrink)

Classical higher-order logic, when utilized as a meta-logic in which various other logics can be shallowly embedded, is well suited for realising a universal logic reasoning approach. Universal logic reasoning in turn, as envisioned already by Leibniz, may support the rigorous formalisation and deep logical analysis of rational arguments within machines. A respective universal logic reasoning framework is described and a range of exemplary applications are discussed. In the future, universal logic reasoning in combination with appropriate, controlled forms of rational (...) argumentation may serve as a communication layer between humans and intelligent machines. (shrink)

This paper concerns the proper definition of embeddings in purely category-theoretical terms. It is argued that plain category theory cannot capture what, in the general case, constitutes an embedding of one structure in another. We discuss three available solutions to this problem: variants of monics, concrete categories, and allegories. The first and last of these are found to be unable to solve the problem, and the second to be philosophically unsatisfactory. Instead, we introduce a theory of forms and relators, which, (...) like allegory theory, attempts to abstract from relation algebras in the way that categories abstract from monoids, but which does not have the shortcomings we have identified in allegories. We show that the theory in question does indeed solve the problem of defining embeddings. (shrink)

Starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. Our axiom sets have been formalized in the Isabelle/HOL interactive proof assistant, and this formalization utilizes a semantically correct embedding of free logic in classical higher-order logic. The modeling and formal analysis of our axiom sets has been significantly supported by series of experiments with automated reasoning tools integrated with Isabelle/HOL. We also address the (...) relation of our axiom systems to alternative proposals from the literature, including an axiom set proposed by Freyd and Scedrov for which we reveal a technical issue (when encoded in free logic where free variables range over defined and undefined objects): either all operations, e.g. morphism composition, are total or their axiom system is inconsistent. The repair for this problem is quite straightforward, however. (shrink)