Results for 'categorial proof theory'

993 found
Order:
  1. Basic proof theory.A. S. Troelstra - 1996 - New York: Cambridge University Press. Edited by Helmut Schwichtenberg.
    This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   160 citations  
  2.  14
    Proof theory: sequent calculi and related formalisms.Katalin Bimbó - 2015 - Boca Raton: CRC Press, Taylor & Francis Group.
    Sequent calculi constitute an interesting and important category of proof systems. They are much less known than axiomatic systems or natural deduction systems are, and they are much less known than they should be. Sequent calculi were designed as a theoretical framework for investigations of logical consequence, and they live up to the expectations completely as an abundant source of meta-logical results. The goal of this book is to provide a fairly comprehensive view of sequent calculi -- including a (...)
    Direct download  
     
    Export citation  
     
    Bookmark   9 citations  
  3.  70
    Truth Values and Proof Theory.Greg Restall - 2009 - Studia Logica 92 (2):241-264.
    I present an account of truth values for classical logic, intuitionistic logic, and the modal logic S5, in which truth values are not a fundamental category from which the logic is defined, but rather, an idealisation of more fundamental logical features in the proof theory for each system. The result is not a new set of semantic structures, but a new understanding of how the existing semantic structures may be understood in terms of a more fundamental notion of (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   22 citations  
  4.  27
    On church's formal theory of functions and functionals: The λ-calculus: connections to higher type recursion theory, proof theory, category theory.Giuseppe Longo - 1988 - Annals of Pure and Applied Logic 40 (2):93-133.
  5.  7
    Category theory for the sciences.David I. Spivak - 2014 - Cambridge, Massachusetts: The MIT Press.
    An introduction to category theory as a rigorous, flexible, and coherent modeling language that can be used across the sciences. Category theory was invented in the 1940s to unify and synthesize different areas in mathematics, and it has proven remarkably successful in enabling powerful communication between disparate fields and subfields within mathematics. This book shows that category theory can be useful outside of mathematics as a rigorous, flexible, and coherent modeling language throughout the sciences. Information is inherently (...)
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  6.  50
    Generality of Proofs and Its Brauerian Representation.Kosta Došen & Zoran Petrić - 2003 - Journal of Symbolic Logic 68 (3):740 - 750.
    The generality of a derivation is an equivalence relation on the set of occurrences of variables in its premises and conclusion such that two occurrences of the same variable are in this relation if and only if they must remain occurrences of the same variable in every generalization of the derivation. The variables in question are propositional or of another type. A generalization of the derivation consists in diversifying variables without changing the rules of inference. This paper examines in the (...)
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  7.  65
    Axiomatizing Category Theory in Free Logic.Christoph Benzmüller & Dana Scott - manuscript
    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 (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  8.  41
    Categories for the Working Philosopher.Elaine M. Landry (ed.) - 2017 - Oxford, England: Oxford University Press.
    This is the first volume on category theory for a broad philosophical readership. It is designed to show the interest and significance of category theory for a range of philosophical interests: mathematics, proof theory, computation, cognition, scientific modelling, physics, ontology, the structure of the world.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   13 citations  
  9.  11
    Set Theory : Boolean-Valued Models and Independence Proofs: Boolean-Valued Models and Independence Proofs.John L. Bell - 2005 - Oxford University Press UK.
    This monograph is a follow up to the author's classic text Boolean-Valued Models and Independence Proofs in Set Theory, providing an exposition of some of the most important results in set theory obtained in the 20th century--the independence of the continuum hypothesis and the axiom of choice. Aimed at research students and academics in mathematics, mathematical logic, philosophy, and computer science, the text has been extensively updated with expanded introductory material, new chapters, and a new appendix on category (...)
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  10.  12
    Constructions of categories of setoids from proof-irrelevant families.Erik Palmgren - 2017 - Archive for Mathematical Logic 56 (1-2):51-66.
    When formalizing mathematics in constructive type theories, or more practically in proof assistants such as Coq or Agda, one is often using setoids. In this note we consider two categories of setoids with equality on objects and show, within intensional Martin-Löf type theory, that they are isomorphic. Both categories are constructed from a fixed proof-irrelevant family F of setoids. The objects of the categories form the index setoid I of the family, whereas the definition of arrows differs. (...)
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  11.  17
    Generality of proofs and its Brauerian representation.Kosta Došen & Zoran Petrić - 2003 - Journal of Symbolic Logic 68 (3):740-750.
    The generality of a derivation is an equivalence relation on the set of occurrences of variables in its premises and conclusion such that two occurrences of the same variable are in this relation if and only if they must remain occurrences of the same variable in every generalization of the derivation. The variables in question are propositional or of another type. A generalization of the derivation consists in diversifying variables without changing the rules of inference.This paper examines in the setting (...)
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  12.  30
    Cut Elimination in Categories.Kosta Došen - 1999 - Dordrecht, Netherland: Springer.
    Proof theory and category theory were first drawn together by Lambek some 30 years ago but, until now, the most fundamental notions of category theory have not been explained systematically in terms of proof theory. Here it is shown that these notions, in particular the notion of adjunction, can be formulated in such as way as to be characterised by composition elimination. Among the benefits of these composition-free formulations are syntactical and simple model-theoretical, geometrical (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  13.  35
    Algebra of proofs.M. E. Szabo - 1978 - New York: sole distributors for the U.S.A. and Canada, Elsevier North-Holland.
    Provability, Computability and Reflection.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   13 citations  
  14.  2
    Categorical Proof-theoretic Semantics.David Pym, Eike Ritter & Edmund Robinson - forthcoming - Studia Logica:1-38.
    In proof-theoretic semantics, model-theoretic validity is replaced by proof-theoretic validity. Validity of formulae is defined inductively from a base giving the validity of atoms using inductive clauses derived from proof-theoretic rules. A key aim is to show completeness of the proof rules without any requirement for formal models. Establishing this for propositional intuitionistic logic raises some technical and conceptual issues. We relate Sandqvist’s (complete) base-extension semantics of intuitionistic propositional logic to categorical proof theory in (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  15. Identity of proofs based on normalization and generality.Kosta Došen - 2003 - Bulletin of Symbolic Logic 9 (4):477-503.
    Some thirty years ago, two proposals were made concerning criteria for identity of proofs. Prawitz proposed to analyze identity of proofs in terms of the equivalence relation based on reduction to normal form in natural deduction. Lambek worked on a normalization proposal analogous to Prawitz's, based on reduction to cut-free form in sequent systems, but he also suggested understanding identity of proofs in terms of an equivalence relation based on generality, two derivations having the same generality if after generalizing maximally (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   33 citations  
  16.  18
    Categories and types in logic, language, and physics: essays dedicated to Jim Lambek on the occasion of his 90th birthday.C. Casadio, Bob Coecke, Michael Moortgat, Philip Scott & Jim Lambek (eds.) - 2014 - New York: Springer.
    For more than 60 years, Jim Lambek has been a profoundly inspirational mathematician, with groundbreaking contributions to algebra, category theory, linguistics, theoretical physics, logic and proof theory. This Festschrift was put together on the occasion of his 90th birthday. The papers in it give a good picture of the multiple research areas where the impact of Jim Lambek's work can be felt. The volume includes contributions by prominent researchers and by their students, showing how Jim Lambek's ideas (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  17.  45
    Discontinuity in categorial grammar.Glyn Morrill - 1995 - Linguistics and Philosophy 18 (2):175 - 219.
    Discontinuity refers to the character of many natural language constructions wherein signs differ markedly in their prosodic and semantic forms. As such it presents interesting demands on monostratal computational formalisms which aspire to descriptive adequacy. Pied piping, in particular, is argued by Pollard (1988) to motivate phrase structure-style feature percolation. In the context of categorial grammar, Bach (1981, 1984), Moortgat (1988, 1990, 1991) and others have sought to provide categorial operators suited to discontinuity. These attempts encounter certain difficulties (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  18.  52
    John L. BELL. Set theory: Boolean-valued models and independence proofs. Oxford: Clarendon press, 2005. Oxford logic guides, no. 47. pp. XXII + 191. ISBN 0-19-856852-5, 987-0-19-856852-0 (pbk). [REVIEW]Patricia Marino - 2006 - Philosophia Mathematica 14 (3):392-394.
    This is the third edition of a book originally published in the 1970s; it provides a systematic and nicely organized presentation of the elegant method of using Boolean-valued models to prove independence results. Four things are new in the third edition: background material on Heyting algebras, a chapter on ‘Boolean-valued analysis’, one on using Heyting algebras to understand intuitionistic set theory, and an appendix explaining how Boolean and Heyting algebras look from the perspective of category theory. The book (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark  
  19.  21
    Cartesian closed Dialectica categories.Bodil Biering - 2008 - Annals of Pure and Applied Logic 156 (2):290-307.
    When Gödel developed his functional interpretation, also known as the Dialectica interpretation, his aim was to prove consistency of first order arithmetic by reducing it to a quantifier-free theory with finite types. Like other functional interpretations Gödel’s Dialectica interpretation gives rise to category theoretic constructions that serve both as new models for logic and semantics and as tools for analysing and understanding various aspects of the Dialectica interpretation itself. Gödel’s Dialectica interpretation gives rise to the Dialectica categories , in: (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  20.  21
    Proof Complexity and Textual Cohesion.Eli Dresner - 2015 - Journal of Logic, Language and Information 24 (1):53-64.
    In the first section of this paper I define a set of measures for proof complexity, which combine measures in terms of length and space. In the second section these measures are generalized to the broader category of formal texts. In the third section of the paper I outline several applications of the proposed theory.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  21.  51
    Composition of Deductions within the Propositions-As-Types Paradigm.Ivo Pezlar - 2020 - Logica Universalis (4):1-13.
    Kosta Došen argued in his papers Inferential Semantics (in Wansing, H. (ed.) Dag Prawitz on Proofs and Meaning, pp. 147–162. Springer, Berlin 2015) and On the Paths of Categories (in Piecha, T., Schroeder-Heister, P. (eds.) Advances in Proof-Theoretic Semantics, pp. 65–77. Springer, Cham 2016) that the propositions-as-types paradigm is less suited for general proof theory because—unlike proof theory based on category theory—it emphasizes categorical proofs over hypothetical inferences. One specific instance of this, Došen points (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  22.  10
    Language in Action: Categories, Lambdas and Dynamic Logic.Johan van Benthem - 1995 - MIT Press.
    Language in Action demonstrates the viability of mathematical research into the foundations of categorial grammar, a topic at the border between logic and linguistics. Since its initial publication it has become the classic work in the foundations of categorial grammar. A new introduction to this paperback edition updates the open research problems and records relevant results through pointers to the literature. Van Benthem presents the categorial processing of syntax and semantics as a central component in a more (...)
    Direct download  
     
    Export citation  
     
    Bookmark   36 citations  
  23.  17
    A Brauerian representation of split preorders.Z. Petric & K. Dosen - 2003 - Mathematical Logic Quarterly 49 (6):579.
    Split preorders are preordering relations on a domain whose composition is defined in a particular way by splitting the domain into two disjoint subsets. These relations and the associated composition arise in categorial proof theory in connection with coherence theorems. Here split preorders are represented isomorphically in the category whose arrows are binary relations and whose composition is defined in the usual way. This representation is related to a classical result of representation theory due to Richard (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  24.  15
    Cellular Categories and Stable Independence.Michael Lieberman, Jiří Rosický & Sebastien Vasey - forthcoming - Journal of Symbolic Logic:1-24.
    We exhibit a bridge between the theory of cellular categories, used in algebraic topology and homological algebra, and the model-theoretic notion of stable independence. Roughly speaking, we show that the combinatorial cellular categories (those where, in a precise sense, the cellular morphisms are generated by a set) are exactly those that give rise to stable independence notions. We give two applications: on the one hand, we show that the abstract elementary classes of roots of Ext studied by Baldwin–Eklof–Trlifaj are (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  25.  35
    Advances in Proof-Theoretic Semantics.Peter Schroeder-Heister & Thomas Piecha (eds.) - 2015 - Cham, Switzerland: Springer Verlag.
    This volume is the first ever collection devoted to the field of proof-theoretic semantics. Contributions address topics including the systematics of introduction and elimination rules and proofs of normalization, the categorial characterization of deductions, the relation between Heyting's and Gentzen's approaches to meaning, knowability paradoxes, proof-theoretic foundations of set theory, Dummett's justification of logical laws, Kreisel's theory of constructions, paradoxical reasoning, and the defence of model theory. The field of proof-theoretic semantics has existed (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   15 citations  
  26.  61
    Second-order abstract categorial grammars as hyperedge replacement grammars.Makoto Kanazawa - 2010 - Journal of Logic, Language and Information 19 (2):137-161.
    Second-order abstract categorial grammars (de Groote in Association for computational linguistics, 39th annual meeting and 10th conference of the European chapter, proceedings of the conference, pp. 148–155, 2001) and hyperedge replacement grammars (Bauderon and Courcelle in Math Syst Theory 20:83–127, 1987; Habel and Kreowski in STACS 87: 4th Annual symposium on theoretical aspects of computer science. Lecture notes in computer science, vol 247, Springer, Berlin, pp 207–219, 1987) are two natural ways of generalizing “context-free” grammar formalisms for string (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  27.  24
    “The Proof Is in the Pudding”: How Mental Health Practitioners View the Power of “Sex Hormones” in the Process of Transition.Jaye Cee Whitehead, Kath Bassett, Leia Franchini & Michael Iacolucci - 2015 - Feminist Studies 41 (3):623-650.
    In lieu of an abstract, here is a brief excerpt of the content:Feminist Studies 41, no. 3. © 2015 by Feminist Studies, Inc. 623 Jaye Cee Whitehead, Kath Bassett, Leia Franchini, and Michael Iacolucci “The Proof Is in the Pudding”: How Mental Health Practitioners View the Power of “Sex Hormones” in the Process of Transition In the United States today, popular discourse touts the power of “sex hormones” and hormone receptors in the brain to chemically produce gender expressions (manifested (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  28.  30
    Internal Diagrams and Archetypal Reasoning in Category Theory.Eduardo Ochs - 2013 - Logica Universalis 7 (3):291-321.
    We can regard operations that discard information, like specializing to a particular case or dropping the intermediate steps of a proof, as projections, and operations that reconstruct information as liftings. By working with several projections in parallel we can make sense of statements like “Set is the archetypal Cartesian Closed Category”, which means that proofs about CCCs can be done in the “archetypal language” and then lifted to proofs in the general setting. The method works even when our archetypal (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  29.  47
    Proof-theoretic Semantics for Classical Mathematics.William W. Tait - 2006 - Synthese 148 (3):603-622.
    We discuss the semantical categories of base and object implicit in the Curry-Howard theory of types and we derive derive logic and, in particular, the comprehension principle in the classical version of the theory. Two results that apply to both the classical and the constructive theory are discussed. First, compositional semantics for the theory does not demand ‘incomplete objects’ in the sense of Frege: bound variables are in principle eliminable. Secondly, the relation of extensional equality for (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  30. Categorial Description: Some Contemporary Metaphysical Issues.Brian Carr - 1987 - Dissertation, University of Exeter (United Kingdom)
    Available from UMI in association with The British Library. ;A form of metaphysical inquiry is in this thesis both illustrated in detail and defended against the charge of issuing in statements which lack cognitive content. 'Categorial description' concerns the fundamental features of our conceptual scheme: the categories described are those of substance, accident, cause, space and time. ;Following Aristotle's distinction between primary and secondary substances, these two notions are addressed as equivalent to those individual or particular things and their (...)
     
    Export citation  
     
    Bookmark  
  31.  58
    Eta-rules in Martin-löf type theory.Ansten Klev - 2019 - Bulletin of Symbolic Logic 25 (3):333-359.
    The eta rule for a set A says that an arbitrary element of A is judgementally identical to an element of constructor form. Eta rules are not part of what may be called canonical Martin-Löf type theory. They are, however, justified by the meaning explanations, and a higher-order eta rule is part of that type theory. The main aim of this paper is to clarify this somewhat puzzling situation. It will be argued that lower-order eta rules do not, (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  32.  14
    Under Lock and Key: A Proof System for a Multimodal Logic.G. A. Kavvos & Daniel Gratzer - 2023 - Bulletin of Symbolic Logic 29 (2):264-293.
    We present a proof system for a multimode and multimodal logic, which is based on our previous work on modal Martin-Löf type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e., a small 2-category. The logic is extended to a lambda calculus, establishing a Curry–Howard correspondence.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  33.  78
    Gaifman's theorem on categorial grammars revisited.Wojciech Buszkowski - 1988 - Studia Logica 47 (1):23 - 33.
    The equivalence of (classical) categorial grammars and context-free grammars, proved by Gaifman [4], is a very basic result of the theory of formal grammars (an essentially equivalent result is known as the Greibach normal form theorem [1], [14]). We analyse the contents of Gaifman's theorem within the framework of structure and type transformations. We give a new proof of this theorem which relies on the algebra of phrase structures and exhibit a possibility to justify the key construction (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  34. Kant’s Deduction and Apperception: Explaining the Categories.Dennis Schulting - 2012 - London and Basingstoke, UK: Palgrave-Macmillan.
    Dennis Schulting offers a thoroughgoing, analytic account of the first half of the Transcendental Deduction of the Categories in the B-edition of Kant's Critique of Pure Reason that is different from existing interpretations in at least one important aspect: its central claim is that each of the 12 categories is wholly derivable from the principle of apperception, which goes against the current view that the Deduction is not a proof in a strict philosophical sense and the standard reading that (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   14 citations  
  35. Reasoning with categorial grammar logic.Raffaella Bernardi - unknown
    The article presents the first results we have obtained studying natural reasoning from a proof-theoretic perspective. In particular we focus our attention on monotonic reasoning. Our system consists of two parts: (i) A Formal Grammar – a multimodal version of classical Categorial Grammar – which while syntactically analysing linguistic expressions given as input, computes semantic information (In particular information about the monotonicity properties of the components of the input string are displayed.); (ii) A simple Natural Logic which derives (...)
     
    Export citation  
     
    Bookmark  
  36.  9
    Elaboration of a theory of resistance.Klaus Wiegerling - 2021 - Filozofija I Društvo 32 (4):641-661.
    The theory of resistance here elaborated is based on considerations current since the 18th century and concern the proof of reality of the external world. However, what is ignored in the course of these proofs are the social, psychological, and in particular the logical aspects of resistance. The idea of a theory of resistance is inspired by tendencies in the philosophy of technology, as well as other current philosophical and scientific lines of thought that obscure their metaphysical (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  37.  40
    Models of Deduction.Kosta Dosen - 2006 - Synthese 148 (3):639-657.
    In standard model theory, deductions are not the things one models. But in general proof theory, in particular in categorial proof theory, one finds models of deductions, and the purpose here is to motivate a simple example of such models. This will be a model of deductions performed within an abstract context, where we do not have any particular logical constant, but something underlying all logical constants. In this context, deductions are represented by arrows (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  38. Algebraic quantum field theory.Hans Halvorson & Michael Mueger - 2006 - In J. Butterfield & J. Earman (eds.), Handbook of the philosophy of physics. Kluwer Academic Publishers.
    Algebraic quantum field theory provides a general, mathematically precise description of the structure of quantum field theories, and then draws out consequences of this structure by means of various mathematical tools -- the theory of operator algebras, category theory, etc.. Given the rigor and generality of AQFT, it is a particularly apt tool for studying the foundations of QFT. This paper is a survey of AQFT, with an orientation towards foundational topics. In addition to covering the basics (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   64 citations  
  39.  36
    N.A. Vasil’ev’s Logical Ideas and the Categorical Semantics of Many-Valued Logic.D. Y. Maximov - 2016 - Logica Universalis 10 (1):21-43.
    Here we suggest a formal using of N.A. Vasil’ev’s logical ideas in categorical logic: the idea of “accidental” assertion is formalized with topoi and the idea of the notion of nonclassical negation, that is not based on incompatibility, is formalized in special cases of monoidal categories. For these cases, the variant of the law of “excluded n-th” suggested by Vasil’ev instead of the tertium non datur is obtained in some special cases of these categories. The paraconsistent law suggested by Vasil’ev (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  40. Hegel on the Proofs and Personhood of God: Studies in Hegel's Logic and Philosophy of Religion by Robert R. Williams. [REVIEW]Kevin J. Harrelson - 2017 - Journal of the History of Philosophy 55 (4):739-740.
    Hegel endorsed proofs of the existence of God, and also believed God to be a person. Some of his interpreters ignore these apparently retrograde tendencies, shunning them in favor of the philosopher's more forward-looking contributions. Others embrace Hegel's religious thought, but attempt to recast his views as less reactionary than they appear to be. Robert Williams's latest monograph belongs to a third category: he argues that Hegel's positions in philosophical theology are central to his philosophy writ large. The book is (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  41.  53
    Advances in the Theory of Argumentation Schemes and Critical Questions.David Godden & Douglas Walton - 2007 - Informal Logic 27 (3):267-292.
    This paper begins a working through of Blair’s (2001) theoretical agenda concerning argumentation schemes and their attendant critical questions, in which we propose a number of solutions to some outstanding theoretical issues. We consider the classification of schemes, their ultimate nature, their role in argument reconstruction, their foundation as normative categories of argument, and the evaluative role of critical questions.We demonstrate the role of schemes in argument reconstruction, and defend a normative account of their nature against specific criticisms due to (...)
    Direct download (13 more)  
     
    Export citation  
     
    Bookmark   20 citations  
  42.  34
    Structuring Co-constructive Logic for Proofs and Refutations.James Trafford - 2016 - Logica Universalis 10 (1):67-97.
    This paper considers a topos-theoretic structure for the interpretation of co-constructive logic for proofs and refutations following Trafford :22–40, 2015). It is notoriously tricky to define a proof-theoretic semantics for logics that adequately represent constructivity over proofs and refutations. By developing abstractions of elementary topoi, we consider an elementary topos as structure for proofs, and complement topos as structure for refutation. In doing so, it is possible to consider a dialogue structure between these topoi, and also control their relation (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  43.  9
    Towards a homotopy domain theory.Daniel O. Martínez-Rivillas & Ruy J. G. B. de Queiroz - 2022 - Archive for Mathematical Logic 62 (3):559-579.
    An appropriate framework is put forward for the construction of $$\lambda $$ -models with $$\infty $$ -groupoid structure, which we call homotopic $$\lambda $$ -models, through the use of an $$\infty $$ -category with cartesian closure and enough points. With this, we establish the start of a project of generalization of Domain Theory and $$\lambda $$ -calculus, in the sense that the concept of proof (path) of equality of $$\lambda $$ -terms is raised to higher proof (homotopy).
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  44.  18
    Metric abstract elementary classes as accessible categories.M. Lieberman & J. Rosický - 2017 - Journal of Symbolic Logic 82 (3):1022-1040.
    We show that metric abstract elementary classes are, in the sense of [15], coherent accessible categories with directed colimits, with concrete ℵ1-directed colimits and concrete monomorphisms. More broadly, we define a notion of κ-concrete AEC—an AEC-like category in which only the κ-directed colimits need be concrete—and develop the theory of such categories, beginning with a category-theoretic analogue of Shelah’s Presentation Theorem and a proof of the existence of an Ehrenfeucht–Mostowski functor in case the category is large. For mAECs (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  45. The scrambling theorem: A simple proof of the logical possibility of spectrum inversion.Donald D. Hoffman - 2006 - Consciousness and Cognition 15 (1):31-45.
    The possibility of spectrum inversion has been debated since it was raised by Locke and is still discussed because of its implications for functionalist theories of conscious experience . This paper provides a mathematical formulation of the question of spectrum inversion and proves that such inversions, and indeed bijective scramblings of color in general, are logically possible. Symmetries in the structure of color space are, for purposes of the proof, irrelevant. The proof entails that conscious experiences are not (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  46.  16
    Homotopy limits in type theory.Jeremy Avigad, Krzysztof Kapulkin & Peter Lefanu Lumsdaine - unknown
    Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to the formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  47. A methodological note on proving agreement between the Elementary Process Theory and modern interaction theories.Cabbolet Marcoen - 2022 - In Marcoen J. T. F. Cabbolet (ed.), And now for something completely different: the Elementary Process Theory. Revised, updated and extended 2nd edition of the dissertation with almost the same title. Utrecht: Eburon Academic Publishers. pp. 373-382.
    The Elementary Process Theory (EPT) is a collection of seven elementary process-physical principles that describe the individual processes by which interactions have to take place for repulsive gravity to exist. One of the two main problems of the EPT is that there is no proof that the four fundamental interactions (gravitational, electromagnetic, strong, and weak) as we know them can take place in the elementary processes described by the EPT. This paper sets forth the method by which it (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  48.  11
    On completeness and cocompleteness in and around small categories.Duško Pavlović - 1995 - Annals of Pure and Applied Logic 74 (2):121-152.
    The simple connection of completeness and cocompleteness of lattices grows in categories into the Adjoint Functor Theorem. The connection of completeness and cocompleteness of Boolean algebras — even simpler — is similarly related to Paré's Theorem for toposes. We explain these relations, and then study the fibrational versions of both these theorems — for small complete categories. They can be interpreted as definability results in logic with proofs-as-constructions, and transferred to type theory.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  49.  89
    Universal grammar as a theory of notation.Humphrey P. Polanen Van Petel - 2006 - Axiomathes 16 (4):460-485.
    What is common to all languages is notation, so Universal Grammar can be understood as a system of notational types. Given that infants acquire language, it can be assumed to arise from some a priori mental structure. Viewing language as having the two layers of calculus and protocol, we can set aside the communicative habits of speakers. Accordingly, an analysis of notation results in the three types of Identifier, Modifier and Connective. Modifiers are further interpreted as Quantifiers and Qualifiers. The (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  50.  54
    The strength of Mac Lane set theory.A. R. D. Mathias - 2001 - Annals of Pure and Applied Logic 110 (1-3):107-234.
    Saunders Mac Lane has drawn attention many times, particularly in his book Mathematics: Form and Function, to the system of set theory of which the axioms are Extensionality, Null Set, Pairing, Union, Infinity, Power Set, Restricted Separation, Foundation, and Choice, to which system, afforced by the principle, , of Transitive Containment, we shall refer as . His system is naturally related to systems derived from topos-theoretic notions concerning the category of sets, and is, as Mac Lane emphasises, one that (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   37 citations  
1 — 50 / 993