The Speakers

Dag Prawitz & Antonio Piccolomini D'Aragona

Dale Miller

Rosalie Iemhoff

Sebastian Enqvist

Sara Negri

Gilda Ferreira & Paulo Oliva

Cristina Sernadas & João Rasga

Tiago de Castro Alves

Dag Prawitz & Antonio Piccolomini D'Aragona

Some variants of proof-theoretic semantics and their relations with

intuitionistic logic and the ecumenical project

We discuss the relationship between different variants of proof-theoretic semantics, particularly those stemming from Dag Prawitz's initial ideas and some subsequent developments due to Peter Schroeder-Heister. We clarify that the known proofs of incompleteness of intuitionistic logic with respect to (monotonic or non-monotonic) proof-theoretic semantics of the latter kind do not apply to Prawitz's original semantics. Nevertheless, we settle negatively the question of the completeness of intuitionistic logic with respect to Prawitz's approach, thus refuting a conjecture he has made. Finally, we point to some features of the discussed variants of proof-theoretic semantics that we consider to be philosophically unsatisfactory, and discuss briefly the relation between proof-theoretic semantics and the ecumenical project.

Dale Miller

The proof theory of linear logic using negative connectives

In linear logic, the negative connectives are those whose right-introduction rules are invertible. I will present a focused, two-sided sequent calculus tailored explicitly for these connectives. Such proofs are constructed using alternating phases of invertible (right-introduction) rules and non-invertible (left-introduction) rules. This proof system helps to illuminate the structural differences between intuitionistic (single-conclusion) and classical (multiple-conclusion) proofs. A primary focus of this study is the emergence of synthetic (large-scale) inference rules and their potential for parallel application. This parallel approach offers a novel methodology for managing disjunctions and existential quantifiers within the context of intuitionistic natural deduction.

Rosalie Iemhoff

Logical Principles and Inferences in Nonclassical Theories

Usually, when one adds nonlogical axioms to a given logic, one expects the logic to remain untouched by this addition, meaning that the set of logical principles valid in the theory equals the set of validities of the logic on which the theory is based. For classical theories this generally holds, but if the logic in question is nonclassical, this is no longer the case. There are well-known examples of arithmetical and set-theoretic theories based on intuitionistic logic in which the law of excluded middle or weaker nonclassical principles hold.

But even if, in the case of nonclassical theories, the underlying logic does not change because of the nonlogical axioms, and their are many examples of such well-behaved constructive theories, actually showing this fact can be quite hard, in contrast to classical theories for which this is mostly a trivial observation.

This talk gives a brief survey of the ideas behind this area of investigation, and discusses some recent results about the logic and the logical inferences of several constructive set theories. The latter is joint work with Robert Passmann. In this talk, these results are merely used as illustrations of the general theme, no advanced knowledge of (constructive) set theory is assumed.

Sebastian Enqvist

TBA

Sara Negri

TBA

Gilda Ferreira & Paulo Oliva

On the Various Translations between Classical, Intuitionistic and Linear Logic

Several different proof translations exist between classical and intuitionistic logic (negative translations), and intuitionistic and linear logic (Girard translations).

Our aim in this talk is to (1) show that these systems can be seen as extensions of intuitionistic linear logic, and (2) use this common logical basis, to present a uniform approach for devising and simplifying proof translations. As we shall see, through a process of systematic “simplifications” we obtain most of the well-known translations in the literature. Based on recent work with Clarence Protin.

Cristina Sernadas & João Rasga

From translations to non-collapsing logic combinations

Prawitz suggested expanding a natural deduction system for intuitionistic logic to include rules for classical logic constructors, allowing both intuitionistic and classical elements to coexist without losing their inherent characteristics. Looking at the added rules from the point of view of the Godel-Gentzen translation, led us to propose a general method for the coexistent combination of two logics when a conservative translation exists from one logic (the source) to another (the host). Then we prove that the combined logic is a conservative extension of the original logics, thereby preserving the unique characteristics of each component logic. In this way there is no collapse of one logic into the other in the combination. We also demonstrate that a Gentzen calculus for the combined logic can be induced from a Gentzen calculus for the host logic by considering the translation. This approach applies to semantics as well. We then establish a general sufficient condition for ensuring that the combined logic is both sound and complete. We apply these principles by combining classical and intuitionistic logics capitalizing on the Godel-Gentzen conservative translation, intuitionistic and S4 modal logics relying on the Godel-McKinsey-Tarski conservative translation, and classical and Jáskowski’s paraconsistent logics taking into account the existence of a conservative translation

Tor Sandqvist

TBA

Iris van der Giessen

Cyclic proofs for Gödel-Löb modal logics: classical and intuitionistic

Gödel–Löb logic (GL) is the classical modal logic of the provability predicate in Peano Arithmetic. An important aspect of GL is that it captures recursive reasoning. Such recursive behavior can be modeled by cyclic or non-wellfounded proofs with infinite branches. For GL, these systems are relatively simple: every infinite branch yields sound reasoning. In intuitionistic versions of GL, this is no longer guaranteed. In this talk, we examine several proof-theoretic approaches to intuitionistic versions of GL, focusing on termination properties and labelled systems. This leads to a highlight of ongoing work with Borja Sierra Miranda and Guillermo Menéndez Turata: we solve the open problem of uniform interpolation for iGL.

Jan von Plato

Connections between classical and intuitionistic propositional logic

Beginning with Gödel, Gentzen, and Prawitz, many ways have been found to connect classical and intuitionistic logic. These connections, old and new, are presented from the point of view of systems of natural deduction.

Carlos Olarte

Modal logics: Semantics Without Worlds

In this talk, we present a non-deterministic semantic framework for modal logics in the modal cube, extending earlier work by Kearns and others. Our approach introduces modular and uniform multi-valued non-deterministic matrices (Nmatrices) tailored to each logic. For all of them, we define a notion of partial valuation and show that it yields sound and complete decision procedures. We additionally reestablish the link between our framework and relational (Kripke-style) semantics, thereby addressing longstanding conjectures concerning the correspondence between modal axioms and semantic conditions in non-deterministic settings. The resulting framework provides a philosophically robust and technically modular alternative to standard possible-world semantics. We conclude with recent developments showing how Nmatrices can be used to provide a semantic account of ecumenical logics.

This is a joint work with Renato Leme, Elaine Pimentel and Marcelo Coniglio.

Tiago de Castro Alves

Ecumenism, provability and proofs

The ecumenical attitude towards logic(s) is based on the general idea of “different logics co-existing in peace”. This phrase is usually interpreted as follows: “different logics” stands for extensionally different relations of logical consequence viz. provability; “co-existing” means holding in a same deductive system i.e. as subsets of this system’s relation of provability; and “in peace” means not only without trivialising the system in which they co-exist, but also not collapsing into one another. So far, it seems that not much attention has been paid to notions of proof viz. proof identity – let alone their co-existence – in ecumenical approaches. Interesting questions are: how important is it to consider proof identity for ecumenical systems? Would it suffice for an ecumenical system to have its own distinctive, non-trivial notion of proof? or should it make room for respectively different, non-collapsing notions of proof identity corresponding to each different logic “under its shelter”? This clearly relates to key conceptual questions: what should count as the proper characterisation of a logic: a specific notion of provability or a specific notion of proof? Even more generally: is logic a discipline about what can be proved or about how one can prove whatever can be proved? Depending on the answers provided, ecumenical systems – and the ecumenical approach to logic as a whole – may be judged differently as to how radically they (can) bring about peaceful co-existence of different logics.

Page updated

Google Sites

Report abuse