Ecumenical Negation at LC2021

 My friend Tim cannot hear me talking about Ecumenical Logic without thinking of Father Ted (below). For friends not from the UK, Father Ted was a very successful comedy series a long, long time ago. They had three seasons, the last one finished the year we came to California, 1998. Apparently, it became a cult series since then, every year they have a Ted Fest and several slogans from the series entered the common spoken language, as Wikipedia tells me. I thought it was funny, but the same kind of funny of Fawlty Towers which is so embarrassing that you have to laugh. I don't like this kind of stuff much, but yes, the family says that I lack a sense of humour altogether.

Anyways, the ecumenical in Ecumenical Logic has nothing to do with priests or religion, funny or non-funny. But it has to do with friends Elaine Pimentel and Luiz Carlos Pereira pictured above. Ecumenical logic is about accepting in the same framework logic systems that tend to be considered exclusive alternatives, like intuitionistic and classical logic. Actually, the label 'ecumenical' is supposed to generalize from this setting, but in reality, this is the case that counts. 

Thus the idea is that we want a system where classical and intuitionistic theorems can be proved and disproved in the respective cases, satisfying as many good proof-theoretical properties as we can have. The issue is of course *which* good properties can we have and how to optimize rules to get as many of these properties, with the most perspicuous rules.

Dag Prawitz approached this problem from a philosophical point of view in his article "Classical versus intuitionistic logic", in the book `Why is this a Proof?' a Festschrift for Luiz Carlos Pereira in 2015. Pereira and Rodriguez proved the normalization of the propositional fragment of Prawitz's system and  provided a possible-worlds semantics for it, proved sound and complete in Normalization, Soundness and Completeness for the Propositional Fragment of Prawitz’ Ecumenical System. Elaine, Luiz Carlos and I have provided sequent calculi for Prawitz's system, which  allows us  a deeper investigation of its proof theoretical properties in An ecumenical notion of entailment. Elaine and Luiz Carlos, together with Sonia Marin and Emerson Sales produced a version of the system extended with constructive Simpson-style modalities  in A pure view of ecumenical modalities.

Now recently we have been discussing the role of negation in the ecumenical system. Luiz Carlos just presented this really nice deck at the Logic Colloquium 2021 in Poland. Now we're working on the paper, which I hope will hit the arXiv soon.

(the cast of Father Ted)