Carl Friedrich von Weizsäcker-Zentrum

Topics

Rules and models (Brîncus)

This topic refers to the course Model-theoretic inferentialism and categoricity (Brîncus). Here is a description and a bibliography for addressing it.

  • J. Hintikka, "Is there completeness in mathematics after Gödel?", in Philosophical topics 17:2, 69-90, pp. 69-73, 77-79 [Hintikka distinguishes between categoricity, deductive and semantic completeness, and argues, among other things, that using a semantically incomplete logical system may be more useful for the aims of the working mathematician. Someone may present Hintikka's view from pp. 77-79 and try to give an inferentialist answer to it]

  • J. Garson, What logic means: from proof theory to model-theoretic semantics, Cambridge University Press, 2013 [pp. 1-24] [This is a technical book on model-theoretic semantics inferentialism. Garson introduces three kinds of models for reading off the meanings of the logical terms from the rules of inference (deductive, local and global). Someone may present the way in which the natural deduction rules fix the classical meanings of the logical terms if we use local models (pp. 38-89). The pages 1-24 are excellent for an introduction to logical inferentialism]

  • J. Warren, Shadows of syntax. Revitalizing logical and mathematical conventionalism, Oxford University Press, 2020 [pp. 78-86, 261-271] [The book argues tha tlogical inferentialism provides us with an explanation of the fact that logical and arithmetical truths are by-products of the syntax of language. Someone may present Warren's argument for accepting the ω-rule (pp. 263-270). Likewise, someone may discuss Warren's argument that open-ended ω-rule provides us with categoricity (pp. 270-271)]

Additional bibliography

  • R. Carnap, Formalization of logic, Harvard University Press, 1943 [pp. 3-6, 94-96, 135-147] [This is a technical book on the non-normal interpretations of propositional and first-order logic. The selected pages, however, offer a general understanding of Carnap's project of attaining a full formalization, i.e., a categorical formalization, of classical logic]

  • J. Murzi & B. Topey, "Categoricity by convention", in Philosophical studies 178, pp. 3391-3420 [pp. 3392-3397] [This is an article on Carnap's categoricity problem. The authors provide a naturalist inferentialist solution to this problem. The paper may be read for a better understanding of (Carnap 1943) and (Garson 2013)]

Proof-theoretical aspects of the Lambek calculus (Catta)

This topic refers to the course An introduction to type logical grammars (Catta). Here is a description and a bibliography for addressing it.

In addition to its linguistic interest, Lambek Calculus has some very interesting properties from the point of view of proof-theory. Lambek Calculus is in fact the ancestor of Linear Logic (developed by Lambek a good 30 years before the appearance of Linear Logic). We propose that students study the proof-theoretic properties of the Lambek Calculus, in particular, strong normalisation, confluence, and the fact - fundamental from a linguistic point of view - that each judgment has a finite number of proofs.

R. Moot and C. Retoré (2012), The logic of categorial grammars: a deductive account of natural language syntax and semantics, Springer, Chapter II. Available at: https://link.springer.com/chapter/10.1007/978-3-642-31555-8_2?noAccess=true

J. Lambek (1958), The mathematics of sentence structure, The American Mathematical Monthly, vol. 65, no. 3, pp. 154-170. Available at: www.cs.cmu.edu/~fp/courses/15816-f16/misc/Lambek58.pdf

Meaning and inference (Cozzo)

This topic refers to the course Inferentialism and its problems (Cozzo). Here is a description and a bibliography for addressing it.

  • R. Brandom, Articulating reasons, Harvard University Press, Cambridge, 2000, Introduction and Chapter 1, pp. 1-77

  • C. Cozzo, "Does epistemological holism leads to meaning holism?", in Topoi 21, 2002, pp. 25-45

  • C. Cozzo, "Cogency and context", in Topoi 38, 2019, pp. 505-516

Justifying elimination rules (Klev)

This topic refers to the course Meaning explanations and dialogues (Klev). Here is a description and a bibliography for addressing it.

Look up the meaning explanations for conjunction, implication, identity and absurdity. Justify the elimination rule for each of these operators on the basis of their meaning explanations.

Here is a list of potential sources to be used for the short presentation:

  • P. Martin-Loöf, Intuitionistic type theory, Bibliopolis, 1984

  • A. Klev, "The justification of identity elimination in Martin-Löf's type theory", in Topoi 38, 2019, pp. 577-590

What, if anything, are meaning explanations good for? (Klev)

This topic refers to the course Meaning explanations and dialogues (Klev)​​​​​​​. Here is a description and a bibliography for addressing it.

  • P. Martin-Löf, "Truth of a proposition, evidence of a judgement, validity of a proof", in Synthese 73, 1987, pp. 407-420 [especially the first three pages]

  • G. Sundholm, "A plea for logical atavism", in Logica Yearbook 2000 [available online at https://hdl.handle.net/1887/10422]

Archive of formal proofs (Koutsoukou-Argyraki)

This topic refers to the course Automated reasoning and proof assistants for mathematics (Koutsoukou-Argyraki). Here is a description and a bibliography for addressing it.

Explore the Archive of Formal Proofs, which is a massive collection of material built on the Isabelle Libraries and mechanically checked in Isabelle. It currently contains over 680 formalisations in a variety of areas (including Mathematics, Logic, Computer Science and Philosophy). Focus on developments of your choice according to your own interests. Describe your experiences.

USEFUL LINKS

Isabelle Webpage (includes installation instructions and a collection of user manuals)

Programming and proving in Isabelle/HOL (main user manual)

The Archive of Formal Proofs

SUPPORT

Subscribe to the Isabelle Zulip Chat

Subscribe to the Isabelle Mailing List

BIBLIOGRAPHY

Isabelle (Koutsoukou-Argyraki)

This topic refers to the course Automated reasoning and proof assistants for mathematics (Koutsoukou-Argyraki). Here is a description and a bibliography for addressing it.

Install Isabelle (optionally: also install the Archive of Formal Proofs, for information see this topic) and experiment with basic examples of your choice according to your interests.

USEFUL LINKS

Isabelle Webpage (includes installation instructions and a collection of user manuals)

Programming and proving in Isabelle/HOL (main user manual)

The Archive of Formal Proofs

SUPPORT

Subscribe to the Isabelle Zulip Chat

Subscribe to the Isabelle Mailing List

BIBLIOGRAPHY

Aristotle’s logic from a dialogical perspective (McConaughey)

This topic refers to the course Dialogical logic, old and new (McConaughey). Here is a description and a bibliography for addressing it.

  • M. Marion and H. Rücker, "Aristotle on universal quantification: a study from the point of view of game semantics", in History and philosophy of logic, 37(3), 2016, pp. 201-229 [this paper argues in favor of a dialogical interpretation of Aristotle's "dictum de omni et de nullo", a very short passage in which Aristotle provides the meaning explanation of universal quantification]

  • M. Crubellier, "The programme of Aristotelian analytics", Revista de humanidades de Valparaiîso 10, 2017, pp. 29-59 [this is a paper in history of philosophy, with few references to modern logic. It argues that Aristotle's syllogisms were intended as a backward movement from conclusion to premises, not, as is usually understood, in a forward movement of inferences, from premises to conclusion]

  • M. Crubellier, M. Marion, Z. McConaughey, S. Rahman, "Dialectic, the dictum de omni and echtesis", History and philosophy of logic, 4(3), 2019, pp. 207-233 [this paper is rather technical on both the historical side (critical survey of the interpretations of Aristotle's echtesis) and the logical side (first formalization of ecthesis using the dialogical variant "immanent reasoning"). However, it argues in favor of an instatiated use of quantification in Aristotle's syllogistic, were content was right beneath the formal surface]

The dialogical framework (McConaughey)

This topic refers to the course Dialogical logic, old and new (McConaughey). Here is a description and a bibliography for addressing it.

  • K. Lorenz, "Meaning postulates and rules of argumentation: remarks concerning the pragmatic tie between meaning (of terms) and truth (of propositions)", in Logic, language and method on polarities in human experience: philosophical papers, De Gruyter, 2010, pp. 71-80 [albeit short, this is paper is challenging. It deals with the philosophical foundations of dialogical logic, as compared to model theory and argumentation theory. The purpose of the paper is two highlight two presuppositions non-dialogical logics take for granted and are not aware of]

  • H. Rückert, "Why dialogical logic?", in H. Wansing (ed.), Essays on non-classical logic, Advances in Logic, vol. 1, 2001, pp. 165-185 [this paper presents the dialogical framework in the Lorenzen and Lorenz tradition. It highlights in a clear manner important principles behind this framework and stresses its usefulness for a pluralist approach, sketching out free logic, paraconsistent logic, modal logic, relevance logic, and their combinations, all within the dialogical framework]

Curry-Howard correspondence (Moriconi)

This topic refers to the course About the Curry-Howard correspondence (Moriconi). Here is a description and a bibliography for addressing it.

  • E. Moriconi, "Steps towards a proof-theoretic semantics", in Topoi, 31 (1), 2012

  • W. A. Howard, "The formulae-as-types notion of construction", in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Academic Press, 1980, pp. 479-491

  • P. Wadler, "Proposition as types", in Communications of the ACM, 58 (12), December 2015, pp. 75-84

  • R. Zach, "The significance of the Curry-Howard Isomorphism", in Philosophy of logic and mathematics, 2019, pp. 313-326

An intutionistic Sheffer's stroke (Pistone-Tranchini)

This topic refers to the course Proof-theoretic harmony (Pistone-Tranchini). Here is a description and a bibliography for addressing it.

In classical propositional logic, Sheffer's stroke is a connective denoting a truth-function in terms of which every other truth-function can be defined. Analogous connectives can be found in the intuitionistic case, i.e. connectives in terms of which all (standard) intuitionistic connectives can be defined. Your task is to provide harmonious natural deduction rules for such a connective, and using them show the definability of the usual connectives.

Bibliography

  • K. Došen, "An intuitionistic Sheffer function", Notre Dame journal of formal logic 26:479-482, 1985

  • P. Schroeder-Heister, "The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony", Studia Logica 102:1185-1216, 2014

Paradox and normalisation failure (Pistone-Tranchini)

This topic refers to the course Proof-theoretic harmony (Pistone-Tranchini). Here is a description and a bibliography for addressing it.

Paradoxical expressions are peculiar in that:

(i) their introduction and elimination rules display the kind of harmony characteristic of the logical connectives;
(ii) but the natural deduction systems containing them fail to normalize.

Whereas some authors argued that non-normalizability is the distinctive feature of paradoxical expression, others have questioned this idea on various grounds. Your task is to present the idea of paradox as non-normalizability and the main objections raised against it.

Bibliography

  • N. Tennant, "Proof and paradox", Dialectica 36(2-3):265-296, 1982

  • P. Schroeder-Heister and L. Tranchini, "Ekman Paradox", Notre Dame journal of formal logic 58(4):567-581, 2017

  • M. Petrolo and P. Pistone, "On paradoxes in normal for", Topoi 38(3):605-617, 2019