Adrian Rezus WSC Book Table of Contents .pdf
À propos / Télécharger Aperçu
Ce document au format PDF 1.5 a été généré par TeX / MiKTeX pdfTeX-1.40.16, et a été envoyé sur fichier-pdf.fr le 21/11/2016 à 21:08, depuis l'adresse IP 85.148.x.x.
La présente page de téléchargement du fichier a été vue 1437 fois.
Taille du document: 229 Ko (7 pages).
Confidentialité: fichier public
Aperçu du document
Witness Structures and Computability
Adrian Rezu¸s (Nijmegen)
May 25, 2016
This is a tentative Table of Contents of a book [in progress] on abstract proof
theory considered from the point of view of a worker on λ-calculus and category theory. Except for the introductory sections [I.1–I.4], the survey contains,
essentially, research done by the author during the last decades (since 1979).1
Chapter I. Background: Basic Concepts and Prerequisites
I.1 An Introduction to λ-calculus and Cartesian Closed Monoids
• I.1.1 Type-free λ-calculi, Combinators, C-monoids and Cartesian Closed Categories
Dana Scott, Joachim Lambek, Karst [C.P.J.] Koymans, Pierre-Louis Curien, Giuseppe
Longo, Andrea Asperti etc.
• I.1.2 Combinator Algebras, λ-algebras and λ-models
Dana Scott, Gordon Plotkin, Erwin Engeler, Albert Meyer, J. Roger Hindley, Giuseppe
Longo, Henk Barendregt, Karst [C. P. J.] Koymans, etc.
• I.1.3 ‘Categorical Models’ of λ-calculus
Henk Barendregt, Karst [C. P. J.] Koymans, Takanori Adachi, Hirofumi Yokouchi,
Pierre-Louis Curien, Bart [B. F. P.] Jacobs, etc.
I.2 Types as Propositions2
• I.2.1 Intuitionistic Logic, BHK and the Curry-Howard Correspondence
The Brouwer-Heyting-Kolmogorov [BHK] interpretation of intuitionistic logic, Curry’s
Functionality Theory, Kleene realisability, William A. Howard, Georg Kreisel et al. on
the meaning of the intuitionistic connectives.
• I.2.2 Propositional and Second-order Quantifiers
Jean-Yves Girard’s ‘System F’ of ‘variable types’ [1970–1971] and John Reynolds’
‘Second-order Typed λ-calculus’ . The proof theory of [intuitionistic] secondorder logic [‘the theory of species’] according to Prawitz [1965, 1971–1973].
• I.2.3 ‘Dependent Types’ and Logic
Curry’s Generalised Functionality Theory, Nicolaas G. de Bruijn’s automath systems,
of’s ‘Constructive Type Theory’ [CTT], Thierry Coquand’s ‘Theory of
1 The dates appearing in square brackets are historical references to original findings and /
or publications by other authors. The projected book is based on published and unpublished
material listed explicitly in the References. Acknowledgement. The corresponding research
has been supported institutionally, in part, by the University of Utrecht (1979–1981), the
Eindhoven University of Technology (1982), the University of Nijmegen (1983), and ZWO
(later NWO), the Dutch National Science Research Foundation (after 1983).
2 For recent critical accounts of typed λ-calculi and the Curry-Howard Correspondence,
including topics not covered in this survey, see also the author’s reviews  and .
etours and Concepts of Reduction
Confluence and normalization theorems: basic results and proof-techniques [Alonzo
Church, J. Barkley Rosser, William Tait, Per Martin-L¨
of, Jean-Yves Girard, J. Roger
Hindley, Barry K. Rosen, Jan Willem Klop, Jean-Jacques Levy, Roel de Vrijer, Kristian
I.4 The Intuitionistic Proof World and Its Conceptual Organigram: Barendregt’s Cubus
I.5 ‘Beyond BHK’. Proofs in Classical Logic: A Preview (1990–1991)
The Kolmogorov-Glivenko translations [1925, 1928–1929]. Dag Prawitz’s  Natural Deduction for classical logic. The origins of λγ-calculi. Classical quantifiers: the
‘extended propositional calculus’ [Peirce-Russell-Le´sniewski-Tarski ‘propositional quantifiers’], classical first-order theories and ‘classical analysis’ [second-order logic].
Chapter II. The Witness Theory of Classical Logic
II.1 ‘An Ancient Logic’
Based on ‘Chrysippus and His Modern Readers’ I (2007, rev. 2016)
II.2 Frege’s Regellogik
On the logic of Frege’s ‘Grundgesetze der Arithmetik’ I . Based on ‘Im Buchstabenparadies’ (2009, rev. 2016).
II.3 ‘Lukasiewicz, Ja´skowski and Natural Deduction’ (2015, rev. 2016)
On Lukasiewicz’s Warsaw Lectures  and Ja´skowski [1927, 1934]. Based on the
paper with the same title.
II.4 Paul Hertz [1922–1929] and Gentzen’s Inauguraldissertation, G¨
II.5 Curry-Howard Correspondence for Classical Logic (1987–2016)
• II.5.1 Basic Witness-theories for Classical Logic
• II.5.2 Equational Double-Negation Extensions
• II.5.3 A Polar Chrysippean Construction
• II.5.4 Inferential Systems: Calculi of λγ-conversion (1987–1988, 1990–1991)
• II.5.5 ‘Separated’ Inferential Systems
A review of the λµ-calculi of Michel Parigot [1991 and later].
• II.5.6 Variations on the ‘Law of Peirce’ and consequentia mirabilis (1990)
• II.5.7 Extensions to Lewis [S4 and S5] modalities (1988, 1991)
II.6 ‘Polish Anomalies’
• II.6.1 Restricted cut [modus ponens].
• II.6.2 Rules Derivability vs Rule Admissibility: A Pseudo-classical Logic
A proof-theoretic analysis of the logic of Henry Hi˙z .
Chapter III. Relevance, Strictness and (Strict) Linearity
III.1 Rosser Combinators and Church’s Strict λ-calculi [λI-calculi] (1979–1981)
III.2 The Proof Theory of Relevance Logics (1979, 1987–1988)
• III.2.1 Pure Relevant Implication R→ and Positive Relevance Logic R→& (1979)
Moh Shaw-Kwei , Alonzo Church , Glen Helman [PhD Diss. 1977].
• III.2.2 Propositional Quantifiers in Relevance Logics
Alonzo Church , Robert K. Meyer et al. [unpublished]3 .
3 See also Alan Ross Anderson, Nuel Belnap Jr et al. Entailment II [Princeton UP, Princeton NJ 1992] and the references listed there to other unpublished papers (1987–1988) by the
present author (as well as by other people), summarized and / or re-used in this Chapter.
• III.2.3 Witness Theory for Non-distributive Relevance Logic LR (1988)
Robert K. Meyer et al. .
• III.2.4 Witness Theory for Boolean Relevance Rogic CR (1988)
Robert K. Meyer & Richard Routley [later: Sylvan] [1973–1974]
• III.2.5 Chrysippus and the Fallacies of Relevance
Based on ‘Chrysippus and His Modern Readers’ II (2016)
III.3 Minimal Strict Linearity
• III.3.1 Cut [‘application’] Definability in BCI-monoids.
• III.3.2 Girard’s ‘Multiplicative Linear Logic’ .
III.4 ‘Strictly Linear λ-calculus and Abelian Groups’
• III.4.1 The Proof-theory of Pure Abelian Logic
Robert K. Meyer and John Slaney [‘Abelian Logic (From A to Z)’ 1979].
• III.4.2 Is (Pure) Abelian Logic Paraconsistent?
III.5 Girard’s ‘Additives’ : Strict Linearity in λπ-calculus (1987)
III.6 Two ‘Modal’ Logics I: Provability Matters (1987)
The conceptual ‘archeology’ of Girard’s ‘[Classical] Linear Logic’ LL : subsystems
and neighbours [mainly relevance logics].4 . Based on ‘Two ‘Modal’ Logics’ (1987).
III.7 Two ‘Modal’ Logics II: Witness Theory (1987)
Curry-Howard for Girard’s LL  and for the ‘Ockham Logic’, a non-strict and
‘modal 5’-extension [with Lewis-like S5-modalities] of LL described axiomatically in
the first part of TML [= III.6]. Based in part on ‘Logic as Communication’ (1988).
Chapter IV. Typed λ-calculus and Higher-order Logic
IV.1 Propositional and Second-order Quantifiers
Based on Nijmegen Lectures (1985–1986) and ‘Impredicative Type Theories’ (1986).
IV.2 ‘Dependent Types’ as Retracts
• IV.2.1 Curry’s Generalized Functionality and ‘Illative Logic’
• IV.2.2 Retract Semantics for ‘Classical’ Automath
Based on joint work with Henk Barendregt (1983). Dana Scott’s ‘Theory of Retracts’
and Applications I.
• IV.2.3 Retract Semantics for Martin L¨
of’s Constructive Type Theory [CTT] (1986)
Based on Nijmegen Lectures (1985–1986) and ‘Semantics of Constructive Type Theory’
(1986). Dana Scott’s ‘Theory of Retracts’ and Applications II.
• IV.2.4 ‘The Taipean Rock Is Close to the Capitol’
Based on ‘Propositions-as-types Revisited’ (1987). Higher-order extensions of de Bruijn’s
Generalized Type Theory. Thierry Coquand’s ‘Theory of Constructions’.
• IV.2.5 Recent Developments on Martin-L¨
On Vladimir Voyevodsky’s Homotopy Type Theory, etc.
Chapter V. Bases, Generators and Axiomatizability5
V.1 Alfred Tarski 
• V.1.1 ‘On a Theorem of Tarski’ (1982)
• V.1.2 ‘Tarski’s Claim, Thirty Years Later’ (2010)
LL is a proper extension of his ‘additive’ logic with Lewis-like S4-modalities.
historical in nature, this Chapter contains a discussion of typical applications of
Witness Theory to axiomatizability problems (survey of results) and to Automated Reasoning,
spelled out in terms of [typed] λ-calculus and combinators.
V.2 Boleslaw Soboci´
nski ‘Z bada¸
n nad teori¸
a dedukcji’ 
Early axiomatizability results (due to Jan Lukasiewicz, Alfred Tarski, Boleslaw Sobocinski, and Mordchaj Wajsberg): an analysis of Soboci´
nski’s ‘Investigations on the theory
of deduction’ [Przegl¸
ad Filozoficzny 35, 1932, pp. 171–193], in λ-calculus terms.
V.3 Morchaj Wajsberg’s ‘Metalogische Beitr¨
age’ [1937, 1939]
V.4 Carew A. Meredith and Arthur N. Prior
V.5 ‘Old Foklore on Singleton λ-calculus Generators’
A review of unpublished results due to Henk Barendregt, Corrado B¨
ohm, J. Barkley
Rosser, Willem L. van der Poel et al.
V.6 Witnessing ‘Axioms for Lattices and Booleaan Algebras’
Sergiu Rudeanu et al. (Cf. S. Rudeanu ‘Axiomele laticilor ¸si ale algebrelor booleene’
[Romanian], Editura Academiei, Bucharest 1963, ‘Axioms for Lattices and Boolean
Algebras’, World Scientific, Singapore 2008 [with R. Padmanabhan], etc.)
V.7 Recent Axiomatizability Results in λ-dressing
Dolph Ulrich [1999, 2007], John Halleck [2010, 2015], Larry Wos et al.
V.8 Other Applications of Witness Theory in Automated Reasoning
Chapter VI. Assorted Topics: Computability and Logic6
VI.1 Turing Computability, λ-definability and Numeral Systems (1981)
VI.2 Ordinal Notations in λ-calculus [Stephen C. Kleene 1937 etc.] (1981)
VI.3 ‘Ordinal Logic’ and Church’s Strict λδ-calculus λδI (1981)
Alonzo Church’s Princeton Lectures [1935–1936], Alan Turing .
VI.4 λ-calculus, Jumps and Non-local Control (1991)
Matthias Felleisen [PhD Diss 1987], Timothy Griffin .
6 Sections VI.1–VI.3 are based on the author’s PhD Diss. (‘Lambda-conversion and Logic’,
Utrecht 1981). Section VI.4 is based on ‘Beyond BHK’ (1991, rev. 1993).
 Henk Barendregt, and Adrian Rezu¸s 1983 Semantics for Classical automath and related
systems, Information and Control [currently: Information and Computation]
59, 1983, pp. 127–147. Also online at the Radboud University Digital Repository, Nijmegen,The Netherlands.)
 Adrian Rezu¸s 1980 Singleton bases for subsets of Λ0K and a result of Alfred Tarski,
Preprint Nr. 150, University of Utrecht, Department of Mathematics, April 1980, ii +
 — 1981 Lambda-conversion and Logic [PhD Dissertation, University of Utrecht
1981], Elinkwijk, Utrecht 1981, ix + 196 pp. (Extended abstract in: Libertas Mathematica [Arlington TX] 2, 1982, pp. 182–185; cf. also Zbl 493.03003.)
 — 1981a Stellingen [Propositions] to the PhD Dissertation , Utrecht, June 4, 1981.
(Dutch version by Henk Barendregt.)
 — 1982 On a theorem of Tarski, Libertas Mathematica [Arlington TX] 2, 1982, pp.
62–95. (Online @ www.equivalences.org.)
 — 1982a On a singleton basis for the set of closed lambda-terms, Libertas Mathematica [Arlington TX] 2, 1982, p. 94. (Solution to an open problem from Carew A.
Meredith. Printed as Appendix to .)
 — 1982b Models for automath, Eindhoven University of Technology, Department of
Mathematics and Computing Science. Draft: September 1982. (A preliminary version
 — 1982c A Bibliography of Lambda-calculi, Combinatory Logics and Related
Topics, Mathematisch Centrum [CWI], Amsterdam 1982, i + 86 pp. [MC Varia] (Online
 — 1983 Abstract automath, Mathematisch Centrum [CWI], Amsterdam 1983 [Mathematical Centre Tracts 160]. (Online in The Automath Archive, Eindhoven, The Netherlands. Also available as an online reprint at the Institutional Digital Repository of CWI,
 — 1983a Orders, Algebraic Lattices, and Scott Domains: An Introduction, Lecture
Notes for a course given at the University of Nijmegen, Faculty of Mathematics and Science, Department of Computer Science, during the Winter Semester 1983. (Typescript:
December 1983, cca 150 pp.)
 — 1983b Constructive type theories and functional programming, (Talk for the Algemeen Informatica Colloquium of the Department of Computer Science, Faculty of
Mathematics and Science, University of Nijmegen, December 1983.)
 — 1986 Impredicative Type Theories, Report TR–KUN–WN–85–1986, University
of Nijmegen. Department of Computer Science.
 — 1986a Semantics of constructive type theory, Libertas mathematica [Arlington
TX] 6, 1986, pp. 1–82. (Reprint: Report TR–KUN–WN–2–1987 (n.s.), University of
Nijmegen, Department of Computer Science.)
 — 1986b automath: Syntax and semantics, Lecture given at the Institute of Advanced
Studies, The Australian National University, The Automated Reasoning Project, Canberra, ACT, September 1986.
 — 1986c Existential types: AUT-Π and variants, Preprint: University of Nijmegen,
Faculty of Mathematics and Science, Department of Computer Science, December 1986,
 — 1987 Propositions-as-types Revisited [1 Higher-order Constructive Type Theory], University of Nijmegen, Department of Computer Science, Report KUN–WN–CS
TR–97–1987, February 1987, 91 pp.
 — 1987a Varieties of Generalized Functionality, University of Nijmegen, Department of Computer Science, Report KUN–WN–CS TR–102–1987, February 1987, 106
pp. (With an Appendix by Peter J. de Bruin.)
 — 1987b Constructions and propositional types, University of Nijmegen, Department
of Computer Science, Internal Report KUN-WN-CS 87–1–1987, April 1987, 64 pp.
 — 1987c Generalized typed lambda-calculi: recent advances, Paper contributed to the
es de L’Acad´
ericaine [ARA] (III-`
eme Section: Math´
ematiques, Physique), Sorbonne, France, June 22–27, 1987. (Summary of a Research
Report NWO-SION on Constructive Mathematics and Functional Programming Languages, NWO [The Dutch National Science Research Foundation], The Hague & Stichting voor Informatica Onderzoek in Nederland [The Dutch Foundation for Research in
Computer Science], Amsterdam, June 1987.)
 — 1987d Two ‘modal’ logics 1, Draft: Paris, June 1987, rev. Nijmegen, August 28, 1990,
21 pp. (Online @ www.equivalences.org.)
 — 1987e Proof programming, Draft: Nijmegen, September 6, 1987, rev. October 3,
1988, 18 pp. (Postulates for [typed] λγ [a first proposal], and a brief discussion of N. G.
de Bruijn’s slogan: Proofs are irrelevant.)
 — 1987f What is a ‘relevant’ proof?, Draft: Nijmegen, September 15, 1987, rev. September 18, 1990. (A review of ‘strict’ λγ-calculi, and the proof-theory of relevant logics.)
 — 1987g Boolean combinators, Draft: Nijmegen, October-November 1987, rev. October
1988. (Combinatory versions of [typed] λγ-calculi. See .)
 — 1987h Programming classical proofs, Draft: Nijmegen, November 18, 1987, 10 pp.
(‘Operational semantics’ for λγ-calculi.)
 — 1987i Two ‘modal’ logics 2, Draft, Nijmegen, December 1987.
 — 1988 Logic as Communication, Preprint: Nijmegen, August 8, 1988, 59 pp.
 — 1988a Local Proof Theory, Preprint: Nijmegen, September 7, 1988, 77 pp.
 — 1988b A type-theoretic approach to classical and non-classical logics, Talk for the
‘Jumelage’ Workshop Typed Lambda-Calculi, University of Nijmegen, November 14–
18, 1988. (One of the earliest public records of research [1986–1988] on λγ-calculi and
the description of the proof-theory of classical, relevance and modal logics, based on
extensions of typed λ-calculus.)
 — 1989 What is a ‘classical’ proof?, Lecture for a GMD-Kolloquium held at the GMD
German National Research Center, Abteilung Karlsruhe [University of Karlsruhe, GMD
ur Programmstrukturen, Computing Department], May 1989. (Revised as a Technical Report: April 1990.)
 — 1989a The type theory of classical logic, Lecture for the Informatica-Colloquium,
University of Groningen, June 1989.
 — 1990 Classical Proofs. λ-calculus Methods in Elementary Proof Theory, Draft
of a monograph, based on Nijmegen lectures, Nijmegen [August 5] 1990. (Online @
 — 1990a Proof-calculi for first order classical logic (extended abstract), Nijmegen, April
8, 1990, 10 pp.
 — 1991 Proof semantics for modal logics [1 Glivenko semantics and epistemic models],
Draft: Nijmegen, June 1991, rev. October 1991.
 — 1991a Beyond BHK, Nijmegen, December 1, 1991, ii + 82 pp. (A slightly revised version [July 20, 1993, updated bibliographically in 2000] appears online @
www.equivalences.org. Extended abstract printed separately as .)
 — 1991b Calculi of λγ-conversion, Informal talk at the University of Rome ‘La Sapienza’,
December 1991. (A brief record of λγ-calculi, based on , .)
 — 1992 Finitism and proof-operations. On a finitistic concept of classical proofconversion, Draft: Nijmegen, June 27, 1992, rev. August 27, 1992, i + 13 pp.
 — 1993 Beyond BHK (extended abstract), in: Henk Barendregt, Marc Bezem, and Jan
Willem Klop (eds.), Dirk van Dalen Festschrift, Utrecht 1993, pp. 114–120 [Quaestiones Infinitae 5 – Publications of the Department of Philosophy, Utrecht University]
(Reprint online @ www.equivalences.org.)
 — 1993a Infinite Lukasiewicz is linear too. Remarks on a theorem of Carew A. Meredith,
Draft: Nijmegen, April 11, 1993, 12 pp.
 — 1993b Witness Structures, Draft of preliminary chapters, Nijmegen, 1993.
 — 2007 An ancient logic, Nijmegen, Summer 2007, rev. May 12, 2016. (First instalment of a projected monograph on ‘Chrysippus and His Modern Readers’. See also .
Preprint online @ www.equivalences.org.)
 — 2009 Im Buchstabenparadies [Gottlob Frege and his Regellogik], Nijmegen, June 13,
2009, rev. May 12, 2016. (Preprint online @ www.equivalences.org.)
 — 2010 Tarski’s claim: thirty years later, Nijmegen, October 1, 2010, rev. May 12, 2016.
(Preprint online @ www.equivalences.org.)
 — 2015 Lukasiewicz, Ja´skowski and Natural Deduction [Curry-Howard for classical logic], Nijmegen, October 2015, rev. May 12, 2016. (Preprint online @
 — 2015a Review of Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira, and Dov M.
Gabbay, The Functional Interpretation of Logical Deduction, Studia Logica 103 (2),
2015, pp. 447–451. (Preprint online @ www.equivalences.org.)
 — 2015b Review of Henk Barendregt, Wil Dekkers, Richard Statman et alii, Lambda
Calculus with Types, 2013, Studia Logica 103 (6), 2015, pp. 1319–1326. (Preprint
online @ www.equivalences.org.)
 — 2015c Old folklore on λ-calculus generators, Nijmegen, May 23, 2015, rev. May 15,
2016. (Preprint online @ www.equivalences.org.)
 — 2016a Chrysippus and the fallacies of relevance (‘Chrysippus and His Modern Readers’ II) [work in progress] 2016.