Łódź-Bochum Workshop

Date & Venue

  • Date: July 2nd and 3rd, 2021.

  • Venue: Online Via Zoom. Please contact Nils for the details.

Speakers

Program

July 2nd

10:15-11:15 Sara Ayhan: "Reduction procedures and the meaning of proofs"

11:30-12:30 Andrzej Indrzejczak: "When iota meets lambda"

Lunch Break

14:00-15:00 Yaroslav Petrukhin: "Natural deduction and normalisation for three- and four-valued Kleene-style logics"

15:15-16:15 Satoru Niki: "Humberstone’s Ω constant and intuitionistic negations"

16:30-17:30 Marek Nowak: "When is a closure system a complete atomic Boolean algebra?"

July 3rd

10:15-11:15 Hitoshi Omori: "Two applications of Herzberger’s semantics"

11:30-12:30 Janusz Kaczmarek: "Which lattice is adequate for Wittgenstein’s logical atomism?"

Lunch Break

14:00-15:00 Daniel Skurt: "Modal Logics or: How I stopped worrying about possible worlds"

15:15-16:15 Heinrich Wansing: "A case-study in logical tetra-lateralism"

16:30-17:30 Michał Zawidski: "Two procedures for deciding non-Fregean identities"

Abstracts

Sara Ayhan "Reduction procedures and the meaning of proofs"

Abstract: What are ‘good’ reduction procedures and why is it important to distinguish these from ‘bad’ ones? It has been argued that from a philosophical point of view, or more specifically a standpoint of proof-theoretic semantics, reduction procedures are closely connected to the question about identity of proofs and that accepting certain reductions would lead to a trivialization of identity of proofs in the sense that every derivation of the same conclusion would have to be identified. (Schroeder-Heister, P. & Tranchini, L. (2017). Ekman’s Paradox. Notre Dame Journal of Formal Logic, 58(4), 567-581.) Therefore, we need to be careful: We cannot just accept any reduction procedure, i.e. any procedure eliminating some kind of detour in a derivation. I agree with this conclusion, however, I will argue that the question, which reductions we accept in our system, is not only important if we see them as generating a theory of proof identity but is also decisive for the more general question whether a proof has meaningful content.

By annotating derivations and reductions with λ-terms in accordance with the Curry-Howard-correspondence, it becomes much clearer what may be wrong with certain reductions. I will give examples of such reductions and show that allowing these would not only trivialize identity of proofs of the same conclusion but that it would allow to reduce a term of one type to the term of an arbitrary other. The λ -calculus and some well-known properties thereof can provide us with directions as to why this happens in these cases but not in the cases of ‘well- behaved’ reductions. If we take reductions as inducing an identity relation then that would force us to identify proofs of different arbitrary formulas. But even if we reject this assumption about proof identity, I will argue that allowing such reductions would render derivations in such a system meaningless.

=====

Andrzej Indrzejczak "When iota meets lambda"

Abstract: Russellian approach to definite descriptions (RDD) was developed in opposition to Meinong’s and Frege’s views. It was presented first in his well known paper “On denoting” and later elaborated in Principia Mathematica. The original Russellian treatment of descriptions represents a kind of eliminativist approach. In contrast to Frege’s view, Russell treated descriptions as a kind of incomplete signs and showed how to get rid of them by means of contextual definitions. However, it is possible to develop his theory with descriptions treated as genuine terms on the basis of the axiom R:

ψ[x/ıyφ] ↔ ∃x(∀y(φ ↔ y = x) ∧ ψ)

However, this solution has disadvantages connected with scoping difficulties if ψ is not elementary. To avoid them Russell introduced additional devices allowing formal control over the scope of description. In fact, the problem is even more serious; ψ must be elementary, since unrestricted version can lead to contradiction.

We can avoid such problems if we enrich the language with lambda-operator and restrict the predication on descriptions to predicate abstracts of the form λxφ. Accordingly, elementary formulae are built from predicate symbols and individual variables only. Definite descriptions are used only as arguments of predicate abstracts, hence the modified version of R is Rλ:

λxψ(ıyφ) ↔ ∃x(∀y(φ ↔ y = x) ∧ ψ)

Pure FOLI (First-order logic with identity and quantifier rules restricted to variables), with added Rλ and β-reduction for lambda-operator saves the essential features of Russellian approach. Moreover it avoids several problems like arbitrary restriction of R to predicate symbols, scoping difficulties or running into contradictions. In the talk we focus on the construction of cut-free sequent calculus for this logic of Russellian descriptions.

=====

Janusz Kaczmarek "Which lattice is adequate for Wittgenstein’s logical atomism?"

Abstract: The lecture will present various lattices that can be used to interpret the main theses of Russell's and Wittgenstein's logical atomism. These will be lattices proposed by Wolniewicz, a Polish formal ontologist who has made a unique formal contribution to the understanding of the theory of logical atomism. Wolniewicz proposes to interpret logical atomism through lattices that have a finite number of dimensions, and in each dimension there are two atomic situations: a given (atomic) state of affairs and its atomic negation. I will show that it is useful to interpret Russell's and Wittgenstein's proposal through lattices with any number of dimensions and any number of atomic states of affairs in each dimension. Moreover, I will transform the language of lattice theory into the language of general topology and show that Wolniewicz's lattices are lattices composed of discrete ontological spaces. The application of the notions and theorems of general topology will make it possible to identify new theorems that are not present in the theory of situations proposed by Wolniewicz.

=====

Satoru Niki "Humberstone’s Ω constant and intuitionistic negations"

Abstract: In his investigation of extensions of intuitionistic logic without deduction theorem, Lloyd Humberstone introduced a constant named Ω. Kripke-semantically, this constant is characterised as being true everywhere in a model, except at the root. In this talk, we shall discuss various aspects of the constant, including how to regain deduction theorem, algebraic semantics, and connections to notions of negation in the intuitionistic context.

=====

Marek Nowak "When is a closure system a complete atomic Boolean algebra?"

Abstract: [pdf]

=====

Hitoshi Omori "Two applications of Herzberger’s semantics" (joint work with Jonas R. B. Arenhart.)

Abstract: In his paper “Dimensions of truth”, Hans Herzberger develops a semantic framework that captures both classical logic and weak Kleene logic through one and the same interpretation. The aim of this talk is to apply the simple idea of Herzberger to two kinds of many-valued semantics. This application will be led by the following two questions.


(i) Is de Finetti conditional a conditional?

(ii) What do CL, K3 and LP disagree about?

=====

Yaroslav Petrukhin "Natural deduction and normalisation for three- and four-valued Kleene-style logics"

Abstract: Kleene (1938) introduced the notion of a regular logic. It is rather technical requirement for logical matrices which has, however, an important and interesting consequence: all regular logics produce partial recursive operations and/or predicates. In the three-valued case four sets of such connectives which produce eight logics depending on the choice of the set of designated values. Among them one may find, e.g., strong and weak Kleene logics, paraconsistent weak Kleene logic, and the Logic of Paradox. Some four-valued generalisations of Kleene’s logics were introduced by Fitting and Tomova. In this talk, we plan to present sound and complete natural deduction formalisations of the logics in question and prove normalisation theorem for them.

=====

Daniel Skurt "Modal Logics or: How I stopped worrying about possible worlds"


Abstract: Our investigation starts with a very weak modal logic, which we refer to as H. The H stands for Humberstone, who introduced this system (cf. p.18, Philosophical Applications of Modal Logic) in the language L = {¬, □, →} as follows:


  • H contains all classical tautologies;

  • H is closed under uniform substitution of arbitrary formulas for propositional variables;

  • H is closed under Modus Ponens.


Based on this background, we will show that not only can H be regarded as some sort of modal logic, besides the fact that there are no conditions specifically required for □, but with methods from Arnon Avron, Michael Dunn, Yuri Ivlev and John Kearns we show how to create a rich universe of modal systems.

=====

Heinrich Wansing "A case-study in logical tetra-lateralism"

Abstract: I will present an expansion of the paraconsistent constructive logic N4 by operators for meaningfulness and nonsensicality. This logics contains three congruence-breaking unary connectives, which gives rise to a tetra-lateral sequent calculus with four different sequent arrows. (This presentation is part of ongoing joint work with Sara Ayhan on logical mulitlateralism.)

=====

Michał Zawidski "Two procedures for deciding non-Fregean identities"

Abstract: Sentential Calculus with Identity (SCI) is a logic extending classical propositional calculus with a new, non-truth-functional connective of sentential identity ≡. In the talk I will present and compare two decision procedures for SCI. The first one is a complexity-optimal labelled tableau calculus, whereas the second one is a non-labelled (internalised) dual tableau calculus which is sound, complete, and terminating, yet not complexity-optimal. Both systems use very different methodologies, which manifests itself not only in the presence of labels in one of them and the lack thereof in the other, but also in disparate sets of rules handling the identity connective and dissimilar techniques used throughout the completeness proofs. I will briefly discuss the technical machinery involved in both procedures as well as their proof-of-concept-implementations. The presented results are joint work with Joanna Golińska-PIlarek and Taneli Huuskonen.

Acknowledgments

Łódź-Bochum Workshop is supported by Ruhr University Bochum as well as the Alexander von Humboldt-Foundation.

Organizers

The workshop is organised by Nils Kürbis. For any inquiries, please write to Nils at: nils [dot] kurbis [at] filhist [dot] uni [dot] lodz [dot] pl.