The Speakers

Abstract: The coreflection principle is an axiom in modal logic that can be considered as a ‘pure’ intuitionistic modal axiom in the following senses. The axiom reads as A -> box A and does not have a meaningful interpretation in classical normal modal logic. Interestingly, it pops up in different intuitionistic modal logics with their own interpretation: epistemic logic, provability logic, and lax logic. Moreover, these intuitionistic modal logics contain only the box and form an interesting study of intuitionistic modalities next to the central discussion of the intuitionistic diamond.

In this talk, I would like to discuss interpretations, axiomatizations and birelational semantics for these logics. In addition, I would like to show some results on the so-called admissible rules for these logics (see, https://doi.org/10.1016/j.apal.2022.103233). Finally, I recently came across an ecumenical treatment in the so-called ‘joint logic of problems and propositions’ introduced by Melikhov (see https://arxiv.org/abs/1312.2575), in which the co-reflection principle plays a role. (slides)

Abstract: One traditional question of “Logical Ecumenism” is the following : when a connective (e.g. implication) is defined by rules (e.g. rules for implication in intuitionistic sequent calculus) which are specific instances of other given rules (e.g. rules for implication in classical sequent calculus), is it possible  to consider that those two sets of rules actually define two connectives (differently noted), able to live in harmony, notably at the computational level (cut-elimination) ? 

When one interprets “intuitionistic’’ and “classical’’ implications in Linear Logic, however, the difference between them is not caught at the level of the implication connective itself (i.e. by distinguishing two implication connectives), but by using differently the two exponentials (the modalities “!” and “?” of Linear Logic, which serve notably to indicate the potential use of left and right structural rules, respectively) when one interprets both implications.

While interpreting/translating the intuitionistic implication only requires the “!’’ exponential, using “?’’ is required to interpret the classical implication. At first sight,  “!’’ appears thus to be “the intuitionistic exponential’’, while “?’’ (needed for right structural operations) appears complementary as “the classical one’’. In a sense, the ecumenist question about the “two implications” is thus converted, in Linear Logic, into ecumenist questions about the “two exponentials”: In which respect, could one say that  “!’’ (resp. “?”) is “the intuitionistic (resp. classical) exponential’’ ? Do they really play such well differentiated roles ? How do they interact dynamically? 

In the presented work, we will keep using the exponential viewpoint to ecumenism, in order to create “intermediate exponentials” and use them to design computational systems of linear logic which are “intermediate” between Intuitionistic LL (ILL) and Classical LL (CLL). Methodologically, the focus is put on how to break the symmetrical interdependency between ! and ? which prevails in CLL, in order to get “!” and the resulting “?” playing well differentiated roles – and this without to loose the computational properties (closure by cut-elimination, atomizability of identity axioms). Four main systems are designed (Dissymmetrical LL, semi-functorial Dissymmetrical LL, semi-specialized Dissymmetrical LL, bi-conclusion LL). (slides) and (slides)

Abstract: We investigate a system of natural deduction in which two negations - one classical, the other constructive - coexist. The way in which this system combines intuitionistic and classical logic provides a unified calculus that codifies both constructive and classical reasoning, on the basis of a uniform pattern of meaning explanations. This setting allows one to avoid the collapse typically engendered by combining classical and intuitionistic negations in a single system. We provide a meaning-theoretic interpretation of the system, which is compatible with the tenets of proof-theoretic semantics. (Joint work with Paolo Pistone)

Abstract: We propose an ecumenical approach to infinitary logic. In particular, we first detail the inadequacy of Kripke style semantics to model infinitary intuitionistic logic and we provide a neighborhood semantics. Next, we introduce a labelled sequent calculus which combines classical and intuitionistic connectives. The resulting system satisfies desirable structural properties such as admissibility of the structural rules of contraction and cut. Classical and intuitionistic infinitary logics emerge as fragments of the labelled system. Finally, the calculus is exploited in order to prove an extension  of the modal embedding to the infinitary setting. (slides)

Abstract: Ecumenical systems are formal codications where two or more logics, even rival logics, can co-exist in peace, and this means that these logics accept and reject the same things, the same rules and the same basic principles. Dag Prawitz proposed a natural deduction ecumenical system, where classical logic and intuitionistic logic are codified in the same system. In this system, the classical logician and the intuitionistic logician would share the universal quantifier, conjunction, negation and the constant for the absurd, but they would each have their own existential quantifier, disjunction and implication, with different meanings. Prawitz main idea is that these different meanings are given by a semantical framework that can be accepted by both parties. That there is a relation between translations and the ecumenical perspective is undeniable. Prawitz himself observes in his paper that Highly relevant to these discussions are the well-known translations of classical predicate logic into intuitionistic predicate logic, first discovered by Gentzen and Gödel. Also of some relevance is the (less well-known) translation of intuitionistic predicate logic into quantifieed classical S4 established by Prawitz & Malmnäs (1968). These translations will not be dealt with here. The emphasis will instead be on meaning-theoretical considerations, but they can be seen to some extent as spelling out the philosophical significance of the fact that classical logic can be translated into intuitionistic logic. But it is also undeniable that the very nature of this relationship is controversial. In the limit, we could even think that in fact there is nothing new in the ecumenical perspective: the classical operators could be eliminated by definitions, like (A →c B) := ¬(A ^ ¬B). The aim of this short note is to show, in the propositional case, that there are interesting relations between the Gödel-Gentzen translation and the ecumenical perspective, but that the later cannot be reduced to the former, much less identified with the former. (slides)

This is joint work with Elaine Pimentel and Valeria de Paiva

Abstract: In the present study, we consider extensions of constructive logic with strong negation by means of unary modal operations. The constructive logic with strong negation has been defined by Nelson and independently by Markov and can be considered a substructural logic. Essentially, this logic is a formalization of the following idea. Usually, we refute a sentence φ either by reductio ad absurdum or by constructing a counter-example of φ. From a constructive point of view, these two ways are not equivalent. In an ecumenical sense, we have two kinds of negation because they obey two different principles: the principle of the third-excluded middle and the principle of non-contradiction. Nelson lattices (N3-lattices) are an algebraic semantics for this logic. They were introduced by H. Rasiowa, and it is known that they form a variety. An interesting result is that every Nelson lattice can be represented as a twist-structure over a Heyting algebra. A Twist structure over a lattice is a construction used by Kalman that allows us to represent an algebra as a subalgebra of a special binary power of the lattice obtained by considering its direct product and its order-dual. From a result of Sendlewski, we know that for every Nelson lattice A, there exists a Heyting algebra H such that A is isomorphic to a subalgebra of a twist structure over H. Indeed, given a Heyting algebra H = (H, ∧, ∨, →, ⊤, ⊥) and a Boolean filter F of H, let R(H, F ) := {(x, y) ∈ H × H : x ∧ y = ⊥ and x ∨ y ∈ F }. Then we have: 1. R(H, F ) = (R(H, F ), ∧, ∨, ∗, ⇒, ⊥, ⊤) is a Nelson lattice, where the operations are defined as follows: • (x, y) ∨ (s, t) = (x ∨ s, y ∧ t), • (x, y) ∧ (s, t) = (x ∧ s, y ∨ t), • (x, y) ∗ (s, t) = (x ∧ s, (x → t) ∧ (s → y)), • (x, y) ⇒ (s, t) = ((x → s) ∧ (t → y), x ∧ t), • ⊤ = (⊤, ⊥), ⊥ = (⊥, ⊤). 2. ¬(x, y) = (y, x), Given a Nelson lattice A, there is a Heyting algebra HA, unique up to isomorphism, and a unique Boolean filter FA of HA such that A is isomorphic to R(HA, FA). In our work, we introduce an extension of the previous twist-structure construction. We consider N3-lattices endowed with two unary modal operators. Finally, we show the connection between the twist representation and the calculus proposed in Pereira and Rodriguez, in the propositional case and its extension to the modal case, using relational semantics. (slides)

This is joint work with María Paula Menchón

Abstract: Recent research on algebraic models of quasi-Nelson logic - a non-involutive generalization of Nelson logic - has brought new attention to a number of classes of algebras which result from enriching (subreducts of) Heyting algebras with a special modal operator known in the literature as a “nucleus”. Among the various algebraic structures thus emerged, for which we employ the umbrella term “intuitionistic modal algebras”, some have been studied since at least the 1970s, usually within the framework of topology and sheaf theory. Others appear more exotic, for their primitive operations arise from algebraic terms of the intuitionistic modal language which have not been previously considered. We for instance investigate the variety of “weak implicative semilattices”, whose members are (non-necessarily distributive) meet semilattices endowed with a nucleus and an implication operation which is not a relative pseudo-complement but satisfies the postulates of Celani and Jansana’s strict implication. A canonical way of obtaining a weak implicative semilattice is by defining, on any pseudo-complemented semilattice, an implication via the term used by Prawitz to introduce the “classical” implication in his Ecumenical System. Likewise the term interpreting the “classical” disjunction within Prawitz’s system may be used to obtain a class of implicative semilattices enriched with a pseudo-disjunction, which is also one of our main object of study. In my talk I will emphasize these connections and discuss where they may lead in future research. For each of the above-mentioned new classes of algebras we have established a representation and a topological duality which generalize the known ones for Heyting algebras enriched with a nucleus. (slides)

This is joint work with Sergio Celani

Abstract: We speak of an ecumenical logical system when it replaces competing systems by unifying them into one system that contains the original systems as parts. Instead of seeing the original systems as being in conflict about which inferences are valid, one takes them to interpret the involved sentences differently and hence to be about different subject matters. The language of the ecumenical system must therefore duplicate some logical or descriptive constants occurring in the original constants, keeping them apart by writing them differently, and then attach meanings to them in a uniform way so that for each constant c in one of the original systems there is a corresponding constant c' in the ecumenical system with a meaning that agrees with how c was used in the original system. Linguistic meaning thus plays a crucial role when formulating an ecumenical system. I will discuss the kind of meaning theory that can be adequate for the purpose of setting up an ecumenical system.