Aim
This year's edition of Logic in Bochum will focus on proof-theoretic semantics, and the aim of the workshop is to discuss and exchange new ideas and recent developments related to the topic of the workshop. The workshop is collocated with the 6th workshop on connexive logics.
Date & Venue
Date: December 5, 2020.
The workshop is planned in a hybrid format. The workshop will take place completely online via Zoom.
(Physical venue) Jahrhunderthalle, Bochum.
(Online) Via Zoom. Please contact Hitoshi for the details.
Speakers
Sara Ayhan (Bochum)
Nils Kürbis (Łódź & Bochum)
Peter Schroeder-Heister (Tübingen)
Luca Tranchini (Tübingen)
Program
13:00--14:00 Sara Ayhan "Uniqueness of logical connectives in a bilateralist setting"
14:10--15:10 Luca Tranchini "Intensional harmony via isomorphism" (joint work with Paolo Pistone)
15:10--15:30 Break
15:30--16:30 Nils Kürbis "A Proposal for a Proof-Theoretic Semantics for Modal Operators"
16:40--17:40 Peter Schroeder-Heister "Popper on deductive logic and logical deduction" (joint work with David Binder and Thomas Piecha)
Abstracts
Sara Ayhan "Uniqueness of logical connectives in a bilateralist setting"
Abstract: In this paper I will show the problems that are encountered when dealing with uniqueness of connectives in a bilateralist setting within the larger framework of proof-theoretic semantics and suggest a solution. Therefore, the logic 2Int is suitable, for which I introduce a sequent calculus system, displaying - just like the corresponding natural deduction system - a consequence relation for provability as well as one dual to provability. I will propose a modification of our characterization of uniqueness incorporating such a duality of consequence relations with which we can maintain uniqueness in a bilateralist setting.
=====
Luca Tranchini "Intensional harmony via isomorphism" (joint work with Paolo Pistone)
Abstract: In this talk we propose a solution to the problem of defining an intensional notion of harmony, that is a notion of harmony capable of discriminating between interderivable collection of rules, and thus more fine-grained than the extensional notions discussed in the literature so far. Our starting point is Schroeder-Heister's recent proposal of defining an (extensional) notion of harmony using interderivability in intuitionistic second-order propositional logic (IPC2). Our proposal consists in replacing interderivability with the notion of isomorphism coming from category theory and the study of typed lambda calculi. The notion of isomorphism is relative to a notion of identity of proof (i.e. an equivalence relation over derivations in IPC2), and to attain a proper account of harmony, we consider isomorphisms in IPC2 relative to a notion of identity of proof capturing a form of parametricity, or uniformity, of proofs of universally quantified propositions.
=====
Nils Kürbis "A Proposal for a Proof-Theoretic Semantics for Modal Operators"
Abstract: According to proof-theoretic semantics, for rules of inference governing a logical connective to define its meaning they must be stable. Stability between the introduction and elimination rules for a connective c obtains if there is a perfect balance between grounds and consequences of formulas with c as main operator: the elimination rules for c license the derivation of all and only the consequences of a formula with c as main operator that are warranted by the grounds for deriving such formulas as specified by the introduction rules for c. It is plausible that if rules of inference are to define the meaning of a connective, they should also satisfy a few other requirements. Typical rules for the modal operators in standard systems of natural deduction fail to do so. Proof-theoretic semantics must therefore look elsewhere for rules that define the meanings of modal operators. I will argue that a formalisation of S4 by Pfenning and Davies comes quite close to what would be required of such a system. I will reformulate their system and also generalise it by using higher-order rules of inference for a connective expressing the valid inference of a formula from a collection of assumptions. A generalised notion of necessity is definable in terms of it. S4 necessity results if the collection of assumptions is empty. The system stays close to Dummett's and Prawitz's philosophical motivations, which are found in the theory of meaning, and defines the meaning of the necessity operator while keeping the unavoidable modifications of their account to a minimum.
=====
Peter Schroeder-Heister "Popper on deductive logic and logical deduction" (joint work with David Binder and Thomas Piecha)
Abstract: Although not very well known (not even among Popperians), Popper provided substantial work on logic and logical deduction. Much of it was published in the late 1940s. An edition of this work together with the edition of a considerable amount of unpublished material will be published together with David Binder and Thomas Piecha in 2021 within the ``Trends in Logic'' series. Poppers logical writings are very remarkable both from the logical aspect and from the point of view of Popperianism. Logically, they make very significant contributions to Gentzen-style deductive systems and to what today is called ``proof-theoretic semantics''. They represent the first full-fledged attempt at an inferential foundation for deductive logic. In this talk I shall try to give an overall assessment of Popper's contribution to deductive logic and also to provide some ideas of how it might fit into Popper's work in general.
Acknowledgments
Logic in Bochum VI is supported by Ruhr University Bochum as well as a Sofja Kovalevskaja Award of the Alexander von Humboldt-Foundation, funded by the German Ministry for Education and Research.
Organizers
The workshop is organized by Heinrich Wansing and Hitoshi Omori. For any inquiries, please write to Hitoshi at: Hitoshi [dot] Omori [at] rub [dot] de.