Results for 'categorial proof theory'

1000+ 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. 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.  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  
  7.  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  
  8.  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  
  9.  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  
  10.  68
    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  
  11.  22
    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.  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  
  14.  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  
  15.  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  
  16.  40
    Proof theory of modal logic.Heinrich Wansing (ed.) - 1996 - Boston: Kluwer Academic Publishers.
    Proof Theory of Modal Logic is devoted to a thorough study of proof systems for modal logics, that is, logics of necessity, possibility, knowledge, belief, time, computations etc. It contains many new technical results and presentations of novel proof procedures. The volume is of immense importance for the interdisciplinary fields of logic, knowledge representation, and automated deduction.
    Direct download  
     
    Export citation  
     
    Bookmark   5 citations  
  17.  1
    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  
  18. 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  
  19.  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  
  20.  13
    Proof theory.Gaisi Takeuti - 1975 - New York, N.Y., U.S.A.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
    This comprehensive monograph is a cornerstone in the area of mathematical logic and related fields. Focusing on Gentzen-type proof theory, the book presents a detailed overview of creative works by the author and other 20th-century logicians that includes applications of proof theory to logic as well as other areas of mathematics. 1975 edition.
    Direct download  
     
    Export citation  
     
    Bookmark   128 citations  
  21.  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  
  22.  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  
  23. Proof Theory of Finite-valued Logics.Richard Zach - 1993 - Dissertation, Technische Universität Wien
    The proof theory of many-valued systems has not been investigated to an extent comparable to the work done on axiomatizatbility of many-valued logics. Proof theory requires appropriate formalisms, such as sequent calculus, natural deduction, and tableaux for classical (and intuitionistic) logic. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   17 citations  
  24.  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  
  25. 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  
  26.  20
    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  
  27.  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  
  28. 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  
  29.  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  
  30.  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  
  31. Jacques Jayez and Lucia M. tovena/free choiceness and non-individuation 1–71 Michael McCord and Arendse bernth/a metalogical theory of natural language semantics 73–116 Nathan salmon/are general terms rigid? 117–134. [REVIEW]Stefan Kaufmann, Conditional Predications, Yoad Winter & Cross-Categorial Restrictions On Measure - 2005 - Linguistics and Philosophy 28:791-792.
     
    Export citation  
     
    Bookmark   1 citation  
  32.  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  
  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.  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  
  36. 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  
  37. Structural Proof Theory.Sara Negri, Jan von Plato & Aarne Ranta - 2001 - New York: Cambridge University Press. Edited by Jan Von Plato.
    Structural proof theory is a branch of logic that studies the general structure and properties of logical and mathematical proofs. This book is both a concise introduction to the central results and methods of structural proof theory, and a work of research that will be of interest to specialists. The book is designed to be used by students of philosophy, mathematics and computer science. The book contains a wealth of results on proof-theoretical systems, including extensions (...)
    Direct download  
     
    Export citation  
     
    Bookmark   119 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.  35
    Proof theory: a selection of papers from the Leeds Proof Theory Programme, 1990.Peter Aczel, Harold Simmons & Stanley S. Wainer (eds.) - 1992 - New York: Cambridge University Press.
    This work is derived from the SERC "Logic for IT" Summer School Conference on Proof Theory held at Leeds University. The contributions come from acknowledged experts and comprise expository and research articles which form an invaluable introduction to proof theory aimed at both mathematicians and computer scientists.
    Direct download  
     
    Export citation  
     
    Bookmark  
  40.  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  
  41. 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  
  42.  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  
  43. 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  
  44.  6
    Proof theory.K. Schütte - 1977 - New York: Springer Verlag.
  45.  8
    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  
  46.  55
    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  
  47.  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  
  48.  70
    Proof Theory for Reasoning with Euler Diagrams: A Logic Translation and Normalization.Ryo Takemura - 2013 - Studia Logica 101 (1):157-191.
    Proof-theoretical notions and techniques, developed on the basis of sentential/symbolic representations of formal proofs, are applied to Euler diagrams. A translation of an Euler diagrammatic system into a natural deduction system is given, and the soundness and faithfulness of the translation are proved. Some consequences of the translation are discussed in view of the notion of free ride, which is mainly discussed in the literature of cognitive science as an account of inferential efficacy of diagrams. The translation enables us (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  49.  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  
  50.  7
    Proof theory and intuitionistic systems.Bruno Scarpellini - 1971 - New York,: Springer Verlag.
1 — 50 / 1000