We present in this paper an abstract categorical logic based on an abstraction of quantifier. More precisely, the proposed logic is abstract because no structural constraints are imposed on models (semantics free). By contrast, formulas are inductively defined from an abstraction both of atomic formulas and of quantifiers. In this sense, the proposed approach differs from other works interested in formalizing the notion of abstract logic and of which the closest to our approach are the institutions, (...) which in addition to be semantics free do not also impose any syntactic contingencies on the structure of formulas. To define the semantical framework in which formulas will be interpreted, we propose to follow the idea from categorical logic which defines the semantical interpretation of formulas from context and as subobjects of an object of a given category. In the spirit of Lawvere’s hyperdoctrines, we use a more abstract notion which generalizes the notion of subobject, standard in category theory: Pitt’s prop-categories. Always in the spirit of categorical logic, we propose a sequent calculus of which we show correctness and completeness for all semantical frameworks defined over any prop-categories. We then study some conditions which allow us to get this completeness result for particular classes of prop-categories. (shrink)

Greek antiquity saw the development of two distinct systems of logic: Aristotle’s theory of the categorical syllogism and the Stoic theory of the hypothetical syllogism. Some ancient logicians argued that hypothetical syllogistic is more fundamental than categorical syllogistic on the grounds that the latter relies on modes of propositional reasoning such asreductio ad absurdum. Peripatetic logicians, by contrast, sought to establish the priority of categorical over hypothetical syllogistic by reducing various modes of propositional reasoning to (...) class='Hi'>categorical form. In the 17th century, this Peripatetic program of reducing hypothetical to categorical logic was championed by Gottfried Wilhelm Leibniz. In an essay titledSpecimina calculi rationalis, Leibniz develops a theory of propositional terms that allows him to derive the rule ofreductio ad absurdumin a purely categorical calculus in which every proposition is of the formA is B. We reconstruct Leibniz’s categorical calculus and show that it is strong enough to establish not only the rule ofreductio ad absurdum, but all the laws of classical propositional logic. Moreover, we show that the propositional logic generated by the nonmonotonic variant of Leibniz’s categorical calculus is a natural system of relevance logic known as RMI$_{{}_ \to ^\neg }$. (shrink)

The interaction between syntax and its semantics is one which has been well studied in categorical logic. The results of this particular study are employed to understand how the brain is able to create meanings. To emphasize the toy character of the proposed model, we prefer to speak of the homunculus brain rather than the brain per se. The homunculus brain consists of neurons, each of which is modeled by a category, and axons between neurons, which are modeled (...) by functors between the corresponding neuron-categories. Each neuron has its own program enabling its working, i.e. a theory of this neuron. In analogy to what is known from categorical logic, we postulate the existence of a pair of adjoint functors, called Lang and Syn, from a category, now called BRAIN, of categories, to a category, now called MIND, of theories. Our homunculus is a kind of “mathematical robot”, the neuronal architecture of which is not important. Its only aim is to provide us with the opportunity to study how such a simple brain-like structure could “create meanings” and perform abstraction operations out of its purely syntactic program. The pair of adjoint functors Lang and Syn model the mutual dependencies between the syntactical structure of a given theory of MIND and the internal logic of its semantics given by a category of BRAIN. In this way, a formal language and its meanings are interwoven with each other in a manner corresponding to the adjointness of the functors Lang and Syn. Higher cognitive functions of abstraction and realization of concepts are also modelled by a corresponding pair of adjoint functors. The categories BRAIN and MIND interact with each other with their entire structures and, at the same time, these very structures are shaped by this interaction. (shrink)

In this book the authors reconcile two different viewpoints of the foundations of mathematics, namely mathematical logic and category theory. In Part I, they show that typed lambda-calculi, a formulation of higher order logic, and cartesian closed categories are essentially the same. In Part II, it is demonstrated that another formulation of higher order logic is closely related to topos theory. Part III is devoted to recursive functions. Numerous applications of the close relationship between traditional logic (...) and the algebraic language of category theory are given. The authors have included an introduction to category theory and develop the necessary logic as required, making the book essentially self-contained. Detailed historical references are provided throughout, and each section concludes with a set of exercises. Thus it is well-suited for graduate courses and research in mathematics and logic. Researchers in theoretical computer science, artificial intelligence and mathematical linguistics will also find this an accessible introduction to a subject of increasing application to these disciplines. (shrink)

5.5. Every topos is linguistic: the equivalence theorem.

n this paper, a non-classical axiomatic system was introduced to classify all moods of Aristotelian syllogisms, in addition to the axiom "Every a is an a" and the bilateral rules of obversion of E and O propositions. This system consists of only 2 definitions, 2 axioms, 1 rule of a premise, and moods of Barbara and Datisi. By adding first-degree propositional negation to this system, we prove that the square of opposition holds without using many of the other rules of (...) classical logic (including double negation elimination). We then show that the Propositional Substructural Logic SLe is the best logic to study Aristotelian Syllogisms. Also, based on the IFLe square of opposition, the rules of conversation and the rules of negation are completely proved in Muzaffar's logic. For this purpose, we used the monadic first-order logic with the same standard deductive apparatus of quantifiers in classical logic, plus the axioms of "some a is an a" and "some not-a is a not-a". Finally, to show that there is no existential commitment to general terms in categorical logic, the Strong Four-Valued Relevant-classical Logic KR4 was used. With the same existential interpretation of the quantifiers and the standard translation of the quarter quantified. (shrink)

There are still on-going debates on what exactly is wrong with Prior’s pathological “tonk.” In this article I argue, on the basis of categorical inferentialism, that two notions of inconsistency ought to be distinguished in an appropriate account of tonk; logic with tonk is inconsistent as the theory of propositions, and it is due to the fallacy of equivocation; in contrast to this diagnosis of the Prior’s tonk problem, nothing is actually wrong with tonk if logic is (...) viewed as the theory of proofs rather than propositions, and tonk perfectly makes sense in terms of the identity of proofs. Indeed, there is fully complete semantics of proofs for tonk, which allows us to link the Prior’s old philosophical idea with contemporary issues at the interface of categorical logic, computer science, and quantum physics, and thereby to expose commonalities between the laws of Reason and the laws of Nature, which are what logic and physics are respectively about. I conclude the article by articulating the ideas of categorical logical positivism and pluralistic unified science as its goal, including the unification of realist and antirealist conceptions of meaning by virtue of the categorical logical basis of metaphysics. (shrink)

We present the paradigm of categories-as-syntax. We briefly recall the even stronger paradigm categories-as-machine-language which led from -calculus to categorical combinators viewed as basic instructions of the Categorical Abstract Machine. We extend the categorical combinators so as to describe the proof theory of first order logic and higher order logic. We do not prove new results: the use of indexed categories and the description of quantifiers as adjoints goes back to Lawvere and has been developed (...) in detail in works of R. Seely. We rather propose a syntactic, equational presentation of those ideas. We sketch the (quasi-equational) categorical structures for dependent types, following ideas of J. Cartmell (contextual categories). All these theories of categorical combinators, together with the translations from -calculi into them, are introduced smoothly, thanks to the systematic use of– - an abstract variable-free notation for -calculus, going back to N. De Bruijn, – - a sequent formulation of the natural deduction. (shrink)

This monograph explores the logical systems of early logicians in the Arabic tradition from a theoretical perspective, providing a complete panorama of early Arabic logic and centering it within an expansive historical context. By thoroughly examining the writings of the first Arabic logicians, al-Fārābī, Avicenna and Averroes, the author analyzes their respective theories, discusses their relationship to the syllogistics of Aristotle and his followers, and measures their influence on later logical systems. Beginning with an introduction to the writings of (...) the most prominent Arabic logicians, the author scrutinizes these works to determine their categorical logic, as well as their modal and hypothetical logics. Where most other studies written on this subject focus on the Arabic logicians’ epistemology, metaphysics, and theology, this volume takes a unique approach by focusing on the actual technical aspects and features of their logics. The author then moves on to examine the original texts as closely as possible and employs the symbolism of modern propositional, predicate, and modal logics, rendering the arguments of each logician clearly and precisely while clarifying the theories themselves in order to determine the differences between the Arabic logicians’ systems and those of Aristotle. By providing a detailed examination of theories that are still not very well-known in Western countries, the author is able to assess the improvements that can be found in the Arabic writings, and to situate Arabic logic within the breadth of the history of logic. This unique study will appeal mainly to historians of logic, logicians, and philosophers who seek a better understanding of the Arabic tradition. It also will be of interest to modern logicians who wish to delve into the historical aspects and progression of their discipline. Furthermore, this book will serve as a valuable resource for graduate students who wish to complement their general knowledge of Arabic culture, logic, and sciences. (shrink)

A system of logic usually comprises a language for which a model-theory and a proof-theory are defined. The model-theory defines the semantic notion of model-theoretic logical consequence (⊨), while the proof-theory defines the proof- theoretic notion of logical consequence (or logical derivability, ⊢). If the system in question is sound and complete, then the two notions of logical consequence are extensionally equivalent. The concept of full formalization is a more restrictive one and requires in addition the preservation of the (...) standard meanings of the logical terms in all the admissible interpretations of the logical calculus, as it is proof-theoretically defined. Although classical first-order logic is sound and complete, its standard formalizations fall short to be full formalizations since they allow non-intended interpretations. This fact poses a challenge for the logical inferentialism program, whose main tenet is that the meanings of the logical terms are uniquely determined by the formal axioms or rules of inference that govern their use in a logical calculus, i.e., logical inferentialism requires a categorical calculus. This paper is the first part of a more elaborated study which will analyze the categoricity problem from its beginning until the most recent approaches. I will first start by describing the problem of a full formalization in the general framework in which Carnap (1934/1937, 1943) formulated it for classical logic. Then, in sections IV and V, I shall discuss the way in which the mathematicians B.A. Bernstein (1932) and E.V. Huntington (1933) have previously formulated and analyzed it in algebraic terms for propositional logic and, finally, I shall discuss some critical reactions Nagel (1943), Hempel (1943), Fitch (1944), and Church (1944) formulated to these approaches. (shrink)

A category theoretic generalization of the theory of algebraizable deductive systems of Blok and Pigozzi is developed. The theory of institutions of Goguen and Burstall is used to provide the underlying framework which replaces and generalizes the universal algebraic framework based on the notion of a deductive system. The notion of a term -institution is introduced first. Then the notions of quasi-equivalence, strong quasi-equivalence and deductive equivalence are defined for -institutions. Necessary and sufficient conditions are given for the quasi-equivalence and (...) the deductive equivalence of two term -institutions, based on the relationship between their categories of theories. The results carry over without any complications to institutions, via their associated -institutions. The -institution associated with a deductive system and the institution of equational logic are examined in some detail and serve to illustrate the general theory. (shrink)

Protoalgebraic logics are characterized by the monotonicity of the Leibniz operator on their theory lattices and are at the lower end of the Leibniz hierarchy of abstract algebraic logic. They have been shown to be the most primitive among those logics with a strong enough algebraic character to be amenable to algebraic study techniques. Protoalgebraic π-institutions were introduced recently as an analog of protoalgebraic sentential logics with the goal of extending the Leibniz hierarchy from the sentential framework to the (...) π-institution framework. Many properties of protoalgebraic logics, studied in the sentential logic framework by Blok and Pigozzi, Czelakowski, and Font and Jansana, among others, have already been adapted in previous work by the author to the categorical level. This work aims at further advancing that study by exploring in this new level some more properties of protoalgebraic sentential logics. (shrink)

An important part of the theory of algebraizable sentential logics consists of studying the algebraic semantics of these logics. As developed by Czelakowski, Blok, and Pigozzi and Font and Jansana, among others, it includes studying the properties of logical matrices serving as models of deductive systems and the properties of abstract logics serving as models of sentential logics. The present paper contributes to the development of the categorical theory by abstracting some of these model theoretic aspects and results from (...) the level of sentential logics to the level of π-institutions. (shrink)

This paper deals with the algebraization of multi-signature equational logic in the context of the modern theory of categorical abstract algebraic logic. Two are the novelties compared to traditional treatments: First, interpretations between different algebraic types are handled in the object language rather than the metalanguage. Second, rather than constructing the type of the algebraizing class of algebras explicitly in an ad-hoc universal algebraic way, the whole clone is naturally constructed using categorical algebraic techniques.

A category theoretic generalization of the theory of algebraizable deductive systems of Blok and Pigozzi is developed. The theory of institutions of Goguen and Burstall is used to provide the underlying framework which replaces and generalizes the universal algebraic framework based on the notion of a deductive system. The notion of a term π-institution is introduced first. Then the notions of quasi-equivalence, strong quasi-equivalence and deductive equivalence are defined for π-institutions. Necessary and sufficient conditions are given for the quasi-equivalence and (...) the deductive equivalence of two term π-institutions, based on the relationship between their categories of theories. The results carry over without any complications to institutions, via their associated π-institutions. The π-institution associated with a deductive system and the institution of equational logic are examined in some detail and serve to illustrate the general theory. (shrink)

Future Logic is an original, and wide-ranging treatise of formal logic. It deals with deduction and induction, of categorical and conditional propositions, involving the natural, temporal, extensional, and logical modalities. Traditional and Modern logic have covered in detail only formal deduction from actual categoricals, or from logical conditionals (conjunctives, hypotheticals, and disjunctives). Deduction from modal categoricals has also been considered, though very vaguely and roughly; whereas deduction from natural, temporal and extensional forms of conditioning has been (...) all but totally ignored. As for induction, apart from the elucidation of adductive processes (the scientific method), almost no formal work has been done. This is the first work ever to strictly formalize the inductive processes of generalization and particularization, through the novel methods of factorial analysis, factor selection and formula revision. This is the first work ever to develop a formal logic of the natural, temporal and extensional types of conditioning (as distinct from logical conditioning), including their production from modal categorical premises. Future Logic contains a great many other new discoveries, organized into a unified, consistent and empirical system, with precise definitions of the various categories and types of modality (including logical modality), and full awareness of the epistemological and ontological issues involved. Though strictly formal, it uses ordinary language, wherever symbols can be avoided. Among its other contributions: a full list of the valid modal syllogisms (which is more restrictive than previous lists); the main formalities of the logic of change (which introduces a dynamic instead of merely static approach to classification); the first formal definitions of the modal types of causality; a new theory of class logic, free of the Russell Paradox; as well as a critical review of modern metalogic. But it is impossible to list briefly all the innovations in logical science — and therefore, epistemology and ontology — this book presents; it has to be read for its scope to be appreciated. (shrink)

In bilateral systems for classical logic, assertion and denial occur as primitive signs on formulas. Such systems lend themselves to an inferentialist story about how truth-conditional content of connectives can be determined by inference rules. In particular, for classical logic there is a bilateral proof system which has a property that Carnap in 1943 called categoricity. We show that categorical systems can be given for any finite many-valued logic using $n$-sided sequent calculus. These systems are understood (...) as a further development of bilateralism—call it multilateralism. The overarching idea is that multilateral proof systems can incorporate the logic of a variety of denial speech acts. So against Frege we say that denial is not the negation of assertion and, with Mark Twain, that denial is more than a river in Egypt. (shrink)

We consider two systems of constructive modal logic which are computationally motivated. Their modalities admit several computational interpretations and are used to capture intensional features such as notions of computation, constraints, concurrency, etc. Both systems have so far been studied mainly from type-theoretic and category-theoretic perspectives, but Kripke models for similar systems were studied independently. Here we bring these threads together and prove duality results which show how to relate Kripke models to algebraic models and these in turn to (...) the appropriate categorical models for these logics. (shrink)

Wójcicki has provided a characterization of selfextensional logics as those that can be endowed with a complete local referential semantics. His result was extended by Jansana and Palmigiano, who developed a duality between the category of reduced congruential atlases and that of reduced referential algebras over a fixed similarity type. This duality restricts to one between reduced atlas models and reduced referential algebra models of selfextensional logics. In this paper referential algebraic systems and congruential atlas systems are introduced, which abstract (...) referential algebras and congruential atlases, respectively. This enables the formulation of an analog of Wójcicki’s Theorem for logics formalized as π-institutions. Moreover, the results of Jansana and Palmigiano are generalized to obtain a duality between congruential atlas systems and referential algebraic systems over a fixed categorical algebraic signature. In future work, the duality obtained in this paper will be used to obtain one between atlas system models and referential algebraic system models of an arbitrary selfextensional π-institution. Using this latter duality, the characterization of fully selfextensional deductive systems among the selfextensional ones, that was obtained by Jansana and Palmigiano, can be extended to a similar characterization of fully selfextensional π-institutions among appropriately chosen classes of selfextensional ones. (shrink)

An algebraization of multi-signature first-order logic without terms is presented. Rather than following the traditional method of choosing a type of algebras and constructing an appropriate variety, as is done in the case of cylindric and polyadic algebras, a new categorical algebraization method is used: The substitutions of formulas of one signature for relation symbols in another are treated in the object language. This enables the automatic generation via an adjunction of an algebraic theory. The algebras of this (...) theory are then used to algebraize first-order logic. (shrink)

Finitely algebraizable deductive systems were introduced by Blok and Pigozzi to capture the essential properties of those deductive systems that are very tightly connected to quasivarieties of universal algebras. They include the equivalential logics of Czelakowski. Based on Blok and Pigozzi’s work, Herrmann defined algebraizable deductive systems. These are the equivalential deductive systems that are also truth-equational, in the sense that the truth predicate of the class of their reduced matrix models is explicitly definable by some set of unary equations. (...) Raftery undertook the task of characterizing the property of truth-equationality for arbitrary deductive systems. In this paper, following Raftery, we extend the notion of truth-equationality for logics formalized as $\pi$-institutions and abstract several of the results that hold for deductive systems in this more general categorical context. (shrink)

We introduce a typed version of the intuitionistic epsilon calculus. We give a categorical semantics of it introducing a class of categories which we call \-categories. We compare our results with earlier ones of Bell :323–337, 1993).

Two classes of π are studied whose properties are similar to those of the protoalgebraic deductive systems of Blok and Pigozzi. The first is the class of N-protoalgebraic π-institutions and the second is the wider class of N-prealgebraic π-institutions. Several characterizations are provided. For instance, N-prealgebraic π-institutions are exactly those π-institutions that satisfy monotonicity of the N-Leibniz operator on theory systems and N-protoalgebraic π-institutions those that satisfy monotonicity of the N-Leibniz operator on theory families. Analogs of the correspondence property of (...) Blok and Pigozzi for π-institutions are also introduced and their connections with preand protoalgebraicity are explored. Finally, relations of these two classes with the (, N)-algebraic systems, introduced previously by the author as an analog of the -algebras of Font and Jansana, and with an analog of the Suszko operator of Czelakowski for π-institutions are also investigated. (shrink)

We analyse the concept of a second-order characterisable structure and divide this concept into two parts—consistency and categoricity—with different strength and nature. We argue that categorical characterisation of mathematical structures in second-order logic is meaningful and possible without assuming that the semantics of second-order logic is defined in set theory. This extends also to the so-called Henkin structures.

Recently, Caleiro, Gon¸calves and Martins introduced the notion of behaviorally algebraizable logic. The main idea behind their work is to replace, in the traditional theory of algebraizability of Blok and Pigozzi, unsorted equational logic with multi-sorted behavioral logic. The new notion accommodates logics over many-sorted languages and with non-truth-functional connectives. Moreover, it treats logics that are not algebraizable in the traditional sense while, at the same time, shedding new light to the equivalent algebraic semantics of logics that (...) are algebraizable according to the original theory. In this paper, the notion of an abstract multi-sorted π-institution is introduced so as to transfer elements of the theory of behavioral algebraizability to the categorical setting. Institutions formalize a wider variety of logics than deductive systems, including logics involving multiple signatures and quantifiers. The framework developed has the same relation to behavioral algebraizability as the classical categorical abstract algebraic logic framework has to the original theory of algebraizability of Blok and Pigozzi. (shrink)

The categoricity problem for a system of logic reveals an asymmetry between the model-theoretic and the proof-theoretic resources of that logic. In particular, it reveals prima facie that the proof-theoretic instruments are insufficient for matching the envisaged model-theory, when the latter is already available. Among the proposed solutions for solving this problem, some make use of new proof-theoretic instruments, some others introduce new model-theoretic constrains on the proof-systems, while others try to use instruments from both sides. On the (...) proof-theoretical side, two main approaches for solving the categoricity problem for propositional classical logic consist in the enforcement of the formal systems of this logic by introducing rules of inference of a new kind. A multiple-conclusions logic allows rules of inference with more than one conclusion, while a bilateralist system contains rules of inference formulated in terms of assertion and rejection. Both these approaches reveal interesting formal features of logical reasoning. This paper analyses some of the advantages and limitations of these two approaches as solutions for a full formalization of logic, i.e., for a categorical formalization. (shrink)

Metalogical properties that have traditionally been studied in the deductive system context (see, e.g., [21]) and transferred later to the institution context [33], are here formulated in the -institution context. Preservation under deductive equivalence of -institutions is investigated. If a property is known to hold in all algebraic -institutions and is preserved under deductive equivalence, then it follows that it holds in all algebraizable -institutions in the sense of [36].

Metalogical properties that have traditionally been studied in the deductive system context (see, e.g., [21]) and transferred later to the institution context [33], are here formulated in the π-institution context. Preservation under deductive equivalence of π-institutions is investigated. If a property is known to hold in all algebraic π-institutions and is preserved under deductive equivalence, then it follows that it holds in all algebraizable π-institutions in the sense of [36].

Wojcicki introduced in the late 1970s the concept of a referential semantics for propositional logics. Referential semantics incorporate features of the Kripke possible world semantics for modal logics into the realm of algebraic and matrix semantics of arbitrary sentential logics. A well-known theorem of Wojcicki asserts that a logic has a referential semantics if and only if it is selfextensional. Referential semantics was subsequently studied in detail by Malinowski and the concept of selfextensionality has played, more recently, an important (...) role in the field of abstract algebraic logic in connection with the operator approach to algebraizability. We introduce and review some of the basic definitions and results pertaining to the referential semantics of π-institutions, abstracting corresponding results from the realm of propositional logics. (shrink)

Using the category of metric spaces as a template, we develop a metric analogue of the categorical semantics of classical/intuitionistic logic, and show that the natural notion of predicate in this “continuous semantics” is equivalent to the a priori separate notion of predicate in continuous logic, a logic which is independently well-studied by model theorists and which finds various applications. We show this equivalence by exhibiting the real interval $[0,1]$ in the category of metric spaces as (...) a “continuous subobject classifier” giving a correspondence not only between the two notions of predicate, but also between the natural notion of quantification in the continuous semantics and the existing notion of quantification in continuous logic.Along the way, we formulate what it means for a given category to behave like the category of metric spaces, and afterwards show that any such category supports the aforementioned continuous semantics. As an application, we show that categories of presheaves of metric spaces are examples of such, and in fact even possess continuous subobject classifiers. (shrink)