Advances in Natural Deduction: A Celebration of Dag Prawitz's Work (Trends in Logic (39))

This Collection Of Papers Celebrating The Contributions Of Swedish Logician Dag Prawitz To Proof Theory, Has Been Assembled From Those Presented At The Natural Deduction Conference Organized In Rio De Janeiro To Honour His seminal research. Dag Prawitz’s Work Forms The Basis Of Intuitionistic Type Theory And His Inversion Principle Constitutes The Foundation Of Most Modern Accounts Of Proof-theoretic Semantics In Logic, Linguistics And Theoretical Computer Science. The Range Of Contributions Includes Material On The Extension Of Natural Deduction With Higher-order Rules, As Opposed To Higher-order Connectives, And A Paper Discussing The Application Of Natural Deduction Rules To Dealing With Equality In Predicate Calculus. The Volume Continues With A Key Chapter Summarizing Work On The Extension Of The Curry-howard Isomorphism (itself A By-product Of The Work On Natural Deduction), Via Methods Of Category Theory That Have Been Successfully Applied To Linear Logic, As Well As Many Other Contributions From Highly Regarded Authorities. With An Illustrious Group Of Contributors Addressing A Wealth Of Topics And Applications, This Volume Is A Valuable Addition To The Libraries Of Academics In The Multiple Disciplines Whose Development Has Been Given Added Scope By The Methodologies Supplied By Natural Deduction. The Volume Is Representative Of The Rich And Varied Directions That Prawitz Work Has Inspired In The Area Of Natural Deduction. Chapter 1. Generalizaed Elimination Inferences; Schroeder-heister, Peter -- Chapter 2. Revisiting Zucker's Work On The Correspondence Between Cut-elimination And Normalisation; Urban, Christian -- Chapter 3. Proofs, Reasoning And The Metamorphosis Of Logic; Joinet, Jean-baptiste -- Chapter 4. Natural Deduction For Equality: The Missing Entity; De Quieroz, Ruy J.g.b. And De Oliveira, Anjolina G -- Chapter 5. Proof-theoretical Conception Of Logic; Legris, Javier -- Chapter 6. On The Structure Of Natural Deduction Derivations For Generally; Vana, Leonardo B., Veloso, Paulo A.s. , And Veloso, Sheila R.m -- Chapter 7. Type Theories From Barendregt's Cube For Theorem Provers; Seldin, Jonathan P -- Chapter 8. What Is Propositional Logic, A Theory Of, If Anything?; Chateaubriand, Oswaldo -- Chapter 9. Categorical Semantics Of Linear Logic For All; De Paiva, Valeria -- Chapter 10. Rough Sets And Proof-theory; Bellin, Gianluigi -- Chapter 11. Decomposition Of Reduction; Zimmermann, Ernst -- Chapter 12. An Approach To General Proof Theory And A Conjecture Of A Kind Of Completeness Of Intuitionistic Logic Revisited; Prawitz, Dag. Edited By Luiz Carlos Pereira, Edward Hermann Haeusler, Valeria De Paiva. Title 4 Copyright 5 Dedication 6 Preface 7 Acknowledgments 13 Contents 14 1 Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus 16 1 Generalized Higher-Level Elimination Rules 17 2 Generalized Standard-Level Elimination Rules 22 3 Comparison of the Higher Level with the Standard-Level Generalized rightarrow Elimination Rules 24 4 Comparison of the Expressive Power of Higher-Level with that of Standard-Level Rules 26 5 The Benefit of Higher-Level Rules: Strong Uniformity and Closure 27 6 Generalized Elimination Rules, Sequent Calculus, and the Proudness Property 31 7 A Sequent Calculus Variant of the Higher-Level Approach 34 8 Implications-as-Rules Versus Implications-as-Links 40 References 42 2 Revisiting Zucker's Work on the Correspondence Between Cut-Elimination and Normalisation 45 1 Introduction 45 2 Natural Deduction 49 3 Sequent Calculus 52 4 The Correspondence Question 57 5 Conclusion 62 References 63 3 Proofs, Reasoning and the Metamorphosis of Logic 65 1 Introduction 65 2 Dynamic Character of Reasoning Versus Static Character of Proofs 68 3 Referential Aspects of Reasoning Versus Inferential Nature of Proofs 70 4 Correctness of Proofs Versus Indeterminacy of Reasoning 72 5 Conclusion 73 References 74 4 Natural Deduction for Equality: The Missing Entity 76 1 Introduction 77 2 Labelled Deduction 84 3 Finale 101 References 102 5 Paul Hertz's Systems of Propositions As a Proof-Theoretical Conception of Logic 105 1 Hertz's Conception of Logic 107 2 Hertz and Gentzen's Sequent Calculus 109 3 Conclusion 111 References 113 6 On the Structure of Natural Deduction Derivations for ``Generally'' 114 1 Introduction 114 2 Logics of `Generally' 116 3 Natural Deduction Systems for `Generally' 120 4 Normalization in Logics for `Generally' 124 5 Minimum Segment in Logics for `Generally' 127 6 Conclusion 135 References 138 7 Type Theories from Barendregt's Cube for Theorem Provers 140 1 Barendregt's λ-Cube 141 2 Representing Logic with Equality 143 3 Adding Unproved Assumptions 145 4 The Consistency of Unproved Assumptions 146 5 Representing Arithmetic 149 6 Representing Sets as Predicates 152 7 Conclusion 153 References 153 8 What is Propositional Logic a Theory of, if Anything? 156 1 Motivation 156 2 Introduction 158 3 Material Implication and the Material Conditional 169 4 Classical Propositional Logic as First-Order Theory 175 5 Material Implication (Continued) 178 6 The Material Conditional (Continued) 180 7 Truth-Value Gaps 183 8 Philosophical Foundations 186 9 Propositional Logic as Theory 189 References 191 9 Categorical Semantics of Linear Logic for All 192 1 Introduction 192 2 The Problem 193 3 Categorical Modeling: What and Why 193 4 Modeling the Modality 195 5 Comparing Models 199 6 Conclusions 202 References 203 10 Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory 204 1 Introduction 204 1.1 Logic for Pragmatics: Dalla Pozza and Garola's Approach 206 2 PART I. Conceptual Analysis: Assertions, Hypotheses, and Conjectures 209 2.1 First Attempt: Assertive and Hypothetical Types 210 2.2 Second Attempt: More General Modal Translations 213 2.3 Bimodal Interpretations of AH 214 2.4 Sequent Calculi for PBL, APBL, AHL 216 2.5 First Conclusions: Assertions and Conjectures 219 3 PART II. Rough-Set Semantics 222 3.1 Rough Sets 222 3.2 Algebra of Regions 226 4 PART III. Proof Theory 227 4.1 Structure of Normal Proofs 228 4.2 Sequents with Tail Formula 229 5 PART IV.Term Assignment for Co-intuitionistic Logic 232 5.1 Term Assignment to the Subtraction Rules in the λ-μ Calculus 233 5.2 A Distributed Term Assignment for the Subtractive Fragment 235 6 A Distributed Term Assignment for Co-intuitionistic Logic nj 237 6.1 Duality Between the Distributed Calculus and the Simply Typed λ Calculus 241 7 Conclusions 242 References 250 11 Decomposition of Reduction 253 1 Natural Deduction and Rewriting 253 2 Abstract Reduction Systems 255 3 Basics of Natural Deduction 258 4 Intuitionistic Logic in Natural Deduction 262 5 Intuitionistic Linear Logic in Natural Deduction 272 References 276 12 An Approach to General Proof Theory and a Conjecture of a Kind of Completeness of Intuitionistic Logic Revisited 278 1 Main Ideas Behind the Conjecture 278 2 The Notion of Validity 280 3 Generalizing the Notion of Validity 282 4 A Modified Approach 284 References 287