Tuesday, March 30, 2021

Natural Deduction is the name of the game


 Last week, on 22nd March 2021 the Nordic Online Seminar had its first meeting and Prof Dag Prawitz gave the first talk on `Validity of inference and argument' (follow the link to join the Nordic Logic Society and be informed of other seminars. They aim to have one per month). It was very nice, there some 160 people in attendance, which is very impressive!

This and the following set of slides (from Peter Schroeder-Heister in 2015 for the celebration of 50 Years of  Natural Deduction) prompted me to post the picture above from the wonderful meeting Natural Deduction in Rio in 2001. (if I keep talking about, maybe Luiz Carlos will re-issue the t-shirts!)

Saturday, March 27, 2021

Seminar re-started!!!

 The seminar has re-started, yay! I'm afraid I had to miss the first meeting (due to some very painful dental issues) but I would like to post the slides of Prof Tiago de Castro Alves, from the  Department of Philosophy, UFMT. Slides here.

(the picture is not associated to the talk. it is here just to remind Luiz Carlos that he needs to be scanning some stuff!)

Tuesday, March 9, 2021

After September 2020


 

The number of logic and philosophy seminars has grown exponentially during these Coronavirus times of ours. I am listing here some of the meetings that compete for our time and disposition with the 'Working Logician'.

There is the Logicians in Quarantine, organized by the

Brazilian Logic Society / Logic Interest Group/Brazilian Computing Society

website at http://sbl.org.br/pmwiki.php/LQ/Quarentena.

The Proof Society Seminar https://www.proofsociety.org/proof-theory-seminar/slides.html

The SuperGroup Logic Seminar https://sites.google.com/view/logicsupergroup/the-logic-supergroup

The Buenos Aires logic group calls its seminar  Seminario de Lógica Iberoamericana (SeLoI), https://ba-logic.com/seloi/

There are many other seminar series, but the point of this post is to list the talks in thee PUC-Rio seminar, organized by Luiz Carlos Pereira as real working seminars for his students. In reverse cronological order the meetings last semester were:

16/12/2020 Title: Trying to understand resource consciousness

Prof. Elaine Pimentel DMAT/UFRN

Abstract:  We look at substructural calculi from a game semantic point of view, guided by certain intuitions about resource conscious and, more specifically, cost conscious reasoning. To this aim, we start with a game, where player I defends a claim corresponding to a (single-conclusion) sequent, while player II tries to refute that claim. Branching rules for additive connectives are modeled by choices of II, while branching for multiplicative connectives leads to splitting the game into parallel subgames, all of which have to be won by player I to succeed. The game comes into full swing by adding cost labels to assumptions, and a corresponding budget. Different proofs of the same end-sequent are interpreted as more or less expensive strategies for I to defend the corresponding claim. This leads to a new kind of labelled calculus, which can be seen as a fragment of SELL (subexponential linear logic). Finally, we generalize the concept of costs in proofs by using a semiring structure, illustrate our interpretation by examples and investigate some proof-theoretical properties.

The talk assumes *no prior knowledge* on games or substructural logic. Only a basic notion of sequent systems is advisable.

This is a joint work with Timo Lang, Carlos Olarte and Christian G. Fermüller.
 

 December 09, 2020 TITLE. A Constructivist Reading of the Epsilon Calculus


SPEAKERS. Mattia Petrolo (UFABC), Elio La Rosa (LMU Munich)

ABSTRACT. The aim of this work is to provide a constructivist reading of Hilbert's epsilon calculus. 
This goal is achieved in two steps, one philosophical and the other logical. First, we investigate 
in which sense the epsilon calculus can be seen, from a broadly Kreiselian perspective, as a way 
of providing a constructive analysis of classical logic and mathematics. In order to highlight the
constructive aspects of this calculus, our strategy is to implement it
in the general proof theoretic setting provided by (a variant of) Gentzen's sequent calculus. 
In particular, a cut-elimination algorithm for a version of the epsilon calculus is provided. 

Thus, in the second part of this work, we show how a given notion of constructivity can be
displayed via the epsilon calculus.

Extra, as it happened in Prof Giorgio Venturi's seminar series 1/12/2020 Title:

A universal graph-theoretic criterion for relevance

Prof Peter Verdée 

 

Abstract

In this talk I present work in progress by my FNRS MIS funded research team (Pilar Terres, Pierre Saint-Germier, Joao Daniel Dantas) working on explanatory inference. We came up with a criterion for relevance of the entailment relation, relative to a given logic. One of the weak criteria of relevance presented in the literature is the principle of variable sharing: if a (multiple conclusion) sequent is relevantly valid then every formula in the sequent needs to have at least one variable in common with the other formulas in the sequent.  I present a couple of cases from which it should be clear that this criterion (while being necessary) certainly is not sufficient for relevance. We solve these problems by analyzing relevance in terms of connectivity. The idea is to say that a sequent is relevantly valid iff a connected graph (of a specific nature) can be established that contains all of the formulas of the sequent. The basis of this idea is the concept of a constitution of a logic. This is a set of sequents that express full logical grounds of all formulas of the language of the logic (the grounded formula of each sequent is underlined, the non-underlined formulas are the partial grounds--examples are "A,B>A&B", "A&B>A" and "A, A->B > B" in the case of classical logic).  The partial grounds (the non-underlined formulas) of each formula determine the way in which formulas of the potentially relevant sequents can be connected to other formulas of the sequent. We will present and motivate the criterion, give a couple of examples, and present some graph-theoretical results concerning this criterion.

 02/12/2020 The pragmatic structure of mathematics

Prof. Giorgio Venturi
 
 
We explore many linguistic facets that permeate mathematical proofs. To do so, we analyze mathematics through the lens of speech act theory, focusing on those illocutionary aspects which are peculiar to the mathematical discourse. Our analysis includes both the single speech acts that occur in proofs and the delicate interplay of such acts.
 

26 y 27 november 2020 Title: A maximalist view on the meaning of logical connectives

Profa. Pilar Terrés

 
Abstract: The aim of this talk is to explore the consequences that minimalism for logical connectives (the view that the meaning is determined by their left and right rules in different sequent calculus languages), together with logical pluralism, has in our undertanding of logical connectives in natural language. I want to suggest an alternative view: the meaning of logical connectives is determined by their left and right rules in the full-structural classical logic, and hence, the meaning of the logical vocabulary is not necessarily determined by their inferential role in the different logics that a pluralist endorses.
 

25/11/2020 Title: The BA plan: how to recapture classicality in the ST-hierarchy

Prof. Eduardo Barrio 
 
Abstract. Anti-exceptionalism about logic is the approach that logical theories have no special epistemological status. Such theories are continuous with scientific theories. Contemporary anti-exceptionalists include data about semantic paradoxes as a part of the logical evidence. Exploring the Buenos Aires plan, the recent development of the metainferential hierarchy of ST-logics shows that there are multiple options to deal with such paradoxes. There is a whole ST-based hierarchy, of which LP and ST itself are only the first steps. The logics in this hierarchy and STω are also options to deal with semantic paradoxes. This talk explores these responses analyzing some reasons to go beyond the first steps. I show that LP, ST and the logics of the ST-hierarchy offer different diagnoses for the same evidence: the inferences and metainferences the agents endorse in the presence of the truth-predicate. But even if the data is not enough to adopt one of these logics, there are other elements to evaluate the revision of classical logic. How close should we be to classical logic? Which logic should be used during the revision? Should a logic be closed under its own rules? How could a logic obey the validities they contain? And mainly, Which is the best explanation of the logical principles to deal with semantic paradoxes? I will argue that, if the answers to these questions are provided by an antiexceptionalist perspective, ST-metainferential logics in general—and STTω in particular—are the best available options.

18/11/20: Reflective Equilibrium and Logical Pluralism

Prof Abílio Rodrigues 

The aim of this talk is to propose a pluralist view of logic that
makes possible a peaceful coexistence between classical logic and some
paraconsistent and paracomplete logics. The central point is to
understand the inference rules of classical, intuitionistic, Nelson's
N3, Belnap-Dunn 4-valued logic, and BLE (the basic logic of evidence)
as a result of two ingredients: i. inferential practices based, in
each case, on a fundamental semantic notion; ii. reflective
equilibrium. The result of combining logical pluralism with reflective
equilibrium is a weak form of revisionism, according to which logic is
not really revised. The idea is rather that different formal systems
are concerned with different properties of propositions, and therefore
are appropriate to different contexts of reasoning. (Joint work with
Marcos Silva)
 
16/11/20: Hermann IV
 
11/11/20: Hermann III

 4/11/20: Hermann II

28/10/20: Título:  Redundancy in huge Natural Deduction proofs or how to obtain polynomial certificates for Non-Hamiltonian graphs.

 
by Edward Hermann Haeusler and Lew Gordeev
 
In this talk, we take the family of normal proofs of the tautologies of the purely implicational minimal logic as a family of super-polynomially bounded or huge sized objects.  We use the notion of (atomic) expanded and mapped normal (EmND) proofs to prove that  almost every huge EmND  proof that has a linearly bounded height is highly redundant.  We show that for almost all proofs of such family there is at least one sub-proof or derivation  that is repeated super-polynomially many times. 
This result points out to a refinement of compression methods previously presented and an alternative and simpler proof that CoNP=NP.

 30 set 2020 10:30 AM São Paulo:  Veloso-type Solutions to Metapuzzles

Prof. Frank Thomas Sautter
Abstract. I introduce a method for solving metapuzzles inspired by
Paulo Veloso's General Theory of Problems. This method is not the
most efficient one, but its virtues include faithful modeling of the
flow of information and logical standardization through the use of the
same first-order predicates in all its applications.







 

14 Oct 2020: Title: It's unlikely that there are good arguments for logical monism

 


professor Diogo H.B. Dias (DF/UENP & DF/USP):

Abstract: The aim of this talk is to investigate some arguments for
logical monism, and to show how, with minor modifications, these
arguments could be used to defend the adequacy of different logics.
Hence, as a defense of logical monism, they all fail. From this
analysis, we'll present a different kind of pluralism, based on the
notion that logic is relative to its domain of application.


Monday, December 21, 2020

Second Semester of Working Logician

(photo by Daniel Schwabe)
 
 I am trying again to list the talks that happened in the Seminar organized by Luiz Carlos Pereira at Phil-PUC. I'm just looking at my inbox, so there are probably some mistakes and confusions. I'd be grateful if people can correct me or send me better links to their webpages and papers.
 
The second semester of the Working Logician Seminar just finished (16 Dec 2020) with a great talk by Elaine Pimentel. She talked about her work on

Title: Trying to understand resource consciousness

Elaine Pimentel DMAT/UFRN

Abstract:  We look at substructural calculi from a game semantic point of view, guided by certain intuitions about resource conscious and, more specifically, cost conscious reasoning. To this aim, we start with a game, where player I defends a claim corresponding to a (single-conclusion) sequent, while player II tries to refute that claim. Branching rules for additive connectives are modeled by choices of II, while branching for multiplicative connectives leads to splitting the game into parallel subgames, all of which have to be won by player I to succeed. The game comes into full swing by adding cost labels to assumptions, and a corresponding budget. Different proofs of the same end-sequent are interpreted as more or less expensive strategies for I to defend the corresponding claim. This leads to a new kind of labelled calculus, which can be seen as a fragment of SELL (subexponential linear logic). Finally, we generalize the concept of costs in proofs by using a semiring structure, illustrate our interpretation by examples and investigate some proof-theoretical properties.

The talk assumes *no prior knowledge* on games or substructural logic. Only a basic notion of sequent systems is advisable. This is a joint work with Timo Lang, Carlos Olarte and Christian G. Fermüller.

***************************
 
Before that, on the 9th Dec we had Prof Mattia Petrolo's talk

TITLE: A Constructivist Reading of the Epsilon Calculus

SPEAKERS. Mattia Petrolo (UFABC), Elio La Rosa (LMU Munich)

ABSTRACT. The aim of this work is to provide a constructivist reading of Hilbert's epsilon calculus. 
This goal is achieved in two steps, one philosophical and the other logical. First, we investigate 
in which sense the epsilon calculus can be seen, from a broadly Kreiselian perspective, as a way 
of providing a constructive analysis of classical logic and mathematics. In order to highlight the
constructive aspects of this calculus, our strategy is to implement it in the general proof theoretic setting provided by (a variant of) Gentzen's sequent calculus. 
In particular, a cut-elimination algorithm for a version of the epsilon calculus is provided. 
Thus, in the second part of this work, we show how a given notion of constructivity can be
displayed via the epsilon calculus.
 
**************************************
On the 2nd of December we had Prof Giorgio Venturi talking about

Title: The pragmatic structure of mathematics

 
We explore many linguistic facets that permeate mathematical proofs. To do so, we analyze mathematics through the lens of speech act theory, focusing on those illocutionary aspects which are peculiar to the mathematical discourse. Our analysis includes both the single speech acts that occur in proofs and the delicate interplay of such acts.
 
*************************************** 
And on 1 de dezembro às 11h00, horário de Brasília (15h00 CET) there was a talk by Prof Peter  Verdee:

Title: A universal graph-theoretic criterion for relevance

Abstract

In this talk I present work in progress by my FNRS MIS funded research team (Pilar Terres, Pierre Saint-Germier, Joao Daniel Dantas) working on explanatory inference. We came up with a criterion for relevance of the entailment relation, relative to a given logic. One of the weak criteria of relevance presented in the literature is the principle of variable sharing: if a (multiple conclusion) sequent is relevantly valid then every formula in the sequent needs to have at least one variable in common with the other formulas in the sequent.  I present a couple of cases from which it should be clear that this criterion (while being necessary) certainly is not sufficient for relevance. We solve these problems by analyzing relevance in terms of connectivity. The idea is to say that a sequent is relevantly valid iff a connected graph (of a specific nature) can be established that contains all of the formulas of the sequent. The basis of this idea is the concept of a constitution of a logic. This is a set of sequents that express full logical grounds of all formulas of the language of the logic (the grounded formula of each sequent is underlined, the non-underlined formulas are the partial grounds--examples are "A,B>A&B", "A&B>A" and "A, A->B > B" in the case of classical logic).  The partial grounds (the non-underlined formulas) of each formula determine the way in which formulas of the potentially relevant sequents can be connected to other formulas of the sequent. We will present and motivate the criterion, give a couple of examples, and present some graph-theoretical results concerning this criterion.

 **************************

Profa. Pilar Terrés (26 y 27 november).
 
Title: A maximalist view on the meaning of logical connectives
 
Abstract: The aim of this talk is to explore the consequences that minimalism for logical connectives (the view that the meaning is determined by their left and right rules in different sequent calculus languages), together with logical pluralism, has in our undertanding of logical connectives in natural language. I want to suggest an alternative view: the meaning of logical connectives is determined by their left and right rules in the full-structural classical logic, and hence, the meaning of the logical vocabulary is not necessarily determined by their inferential role in the different logics that a pluralist endorses.
 

 **************************

Prof. Eduardo Barrio (25/11/2020) 

Title: The BA plan: how to recapture classicality in the ST-hierarchy

 
Abstract. Anti-exceptionalism about logic is the approach that logical theories have no special epistemological status. Such theories are continuous with scientific theories. Contemporary anti-exceptionalists include data about semantic paradoxes as a part of the logical evidence. Exploring the Buenos Aires plan, the recent development of the metainferential hierarchy of ST-logics shows that there are multiple options to deal with such paradoxes. There is a whole ST-based hierarchy, of which LP and ST itself are only the first steps. The logics in this hierarchy and STω are also options to deal with semantic paradoxes. This talk explores these responses analyzing some reasons to go beyond the first steps. I show that LP, ST and the logics of the ST-hierarchy offer different diagnoses for the same evidence: the inferences and metainferences the agents endorse in the presence of the truth-predicate. But even if the data is not enough to adopt one of these logics, there are other elements to evaluate the revision of classical logic. How close should we be to classical logic? Which logic should be used during the revision? Should a logic be closed under its own rules? How could a logic obey the validities they contain? And mainly, Which is the best explanation of the logical principles to deal with semantic paradoxes? I will argue that, if the answers to these questions are provided by an antiexceptionalist perspective, ST-metainferential logics in general—and STTω in particular—are the best available options. 

**********************************

 Professor Abílio Rodrigues (18/11/2020)

Title: Reflective Equilibrium and Logical Pluralism


The aim of this talk is to propose a pluralist view of logic that
makes possible a peaceful coexistence between classical logic and some
paraconsistent and paracomplete logics. The central point is to
understand the inference rules of classical, intuitionistic, Nelson's
N3, Belnap-Dunn 4-valued logic, and BLE (the basic logic of evidence)
as a result of two ingredients: i. inferential practices based, in
each case, on a fundamental semantic notion; ii. reflective
equilibrium. The result of combining logical pluralism with reflective
equilibrium is a weak form of revisionism, according to which logic is
not really revised. The idea is rather that different formal systems
are concerned with different properties of propositions, and therefore
are appropriate to different contexts of reasoning. (Joint work with
Marcos Silva)

 ********************************

We started this second half of the Seminar with four presentations by Prof Hermann Haeusler,

Título:  Redundancy in huge Natural Deduction proofs or how to obtain polynomial certificates for Non-Hamiltonian graphs

 
by Edward Hermann Haeusler and Lew Gordeev
 
In this talk, we take the family of normal proofs of the tautologies of the purely implicational minimal logic as a family of super-polynomially bounded or huge sized objects.  We use the notion of (atomic) expanded and mapped normal (EmND) proofs to prove that  almost every huge EmND  proof that has a linearly bounded height is highly redundant.  We show that for almost all proofs of such family there is at least one sub-proof or derivation  that is repeated super-polynomially many times. 
This result points out to a refinement of compression methods previously presented and an alternative and simpler proof that CoNP=NP.

Sunday, September 20, 2020

"Working Logician" is BACK!



During these difficult times of pandemic, one of the silver linings has been the creation of several online Logic seminars. Luiz Carlos Pereira (Lattes) created one at Phil-PUC that he called simply "Proof Theory". I asked him to rename it as "Working Logician" because `proof theory' is not descriptive enough and when I search for it in my email, lots and lots of things appear!

I don't know if the renaming will work for everyone, but in any case, let me list some of the talks that we've had since the seminar transitioned to online due to the pandemic and hence I could participate. 

I will probably misremember and forget some stuff, so please give me a hand and send corrections and additions, please!

First, a note of the conference where the picture above was taken:

 O evento ocorreu em Recife nos dias 9 a 11 de outubro de 2019, organizado pelo prof. Marcos Silva (UFPE/CNPq). No canal do youtube da SBFA os vídeos das palestras proferidas pelos prof. Dr. Fernando Raul (UFPE), prof. Dr. João Marcos (UFRN) e prof. Dr. Luiz Carlos Pereira (PUC-Rio/UERJ/CNPq).

Now a list of seminars of "PUC Proof Theory or Working Logician":


20 May and 27th May: Gisele Secco on "Diagrams and Computers in the Proof of the Four-Colour Theorem",  5th International Meeting of the APMP Zurich, Switzerland | January 18 – 21, 2020.


 3rd June, 11th June, 17 June: Tiago Rezende de Castro Alves on SYNONYMY AND IDENTITY OF PROOFS: A Philosophical Essay, doctoral thesis Tuebingen


1st July: John Mumma  (title/slides, please?)


8th July: Wagner Sanz (08/07/2020): Máquinas euclidianas: teoria geral de problemas


20th July: Alberto Naibo "Gentzen on proof theory and projective geometry"


16 Sept: Marcos Silva "Revisão da Lógica e Equilíbrio Reflexivo"



Wednesday, July 20, 2016

History is always difficult

This is a picture of Stanisław Jaśkowski (April 22, 1906, Warsaw – November 16, 1965, Warsaw) from Wikipedia, of course.
Jaśkowski is (as discussed in class)  one of the founders of natural deduction, which he described completely independently from Gerhard Gentzen in the 1930s.

Wikipedia  says that Gentzen's approach initially became more popular with logicians because it could be used to prove the cut-elimination theorem. But Jaśkowski's is closer to the way that proofs are done in practice.

This doesn't ring true to me (Valeria). I think only later logicians got interested in cut-elimination and that Jaśkowski's natural deduction system, which later came to be known as Fitch-style natural deduction,  is easier to typeset and hence more adaptable to textbooks.

But at least least his original paper is available from Wikipedia (On the Rules of Suppositions in Formal Logic Studia Logica 1, 1934 pp. 5–32; reprinted in: Storrs McCall (ed.), Polish logic 1920-1939, Oxford University Press, 1967 pp. 232–258) and young logicians can compare his article with Gentzen's.

Another major controversy in the earlier years of Natural Deduction was the one about the exact rules for the quantifiers in first-order logic. Much ink was spilled on that one too.

For my part I am much more interested in the issue of the trade-offs that one must make to extend Natural Deduction to Modal Logics and to substructural logics. Some incipient discussion can be found in Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic (G. Bellin, V. de Paiva and E. Ritter), In Methods for Modalities 2001, Amsterdam, November 2001. (pdf).

Need to add the reference to  Jaśkowski's paper and to von Neumann's discussion to our bibliography. Also need to read these, thanks for the historical insights Luiz Carlos. Here are the slides from the first lecture of the course.

Sunday, July 17, 2016

References are Hard

Luiz Carlos and Hermann will produce cleaned up versions of the slides for the course, separated by days, i.e. Lecture 1,  Lecture 2, ..., Lecture 5.  Meanwhile here are some references that Luiz Carlos decided to add to his three classes.

(i) References for Prawitz' ecumenical system:
[1] Prawitz, Dag – Classical versus intuitionistic logic, in Why is this a proof, College Books, Tributes 27, 2015, pp. 15 – 32.
[2] Dowek, Gilles – On the definition of the classical connectives and quantifiers, in Why is this a proof, College Books, Tributes 27, 2015, pp. 228 - 238.
[3] Krauss, P.H. - A constructive interpretation of classical mathematics, Mathematische Schriften Kassel, preprint No. 5/92, 1992.

(ii) References for Ferreira's system Fat:
[1]  The faithfulness  of atomic polymorphism, Fernando Ferreira e Gilda Ferreira, Trends in Logic (2014)
[2]  Atomic polymorphism, Fernando Ferreira e Gilda Ferreira, JSL, vol. 76 (2013)
[3]  Commuting conversions vs. the standard conversions of the “good connectives", Fernando Ferreira e Gilda Ferreira, Studia Logica, vol. 92 (2009).

(iii) Reference for schematic rules:
Schröder-Heister, Peter – Generalized elimination inferences, higher-level rules,
and the implications-as- rules interpretation of the sequent calculus, in Advances in Natural Deduction – a celebration of Dag Prawitz’ work, (eds) Luiz Carlos
Pereira, Edward Hermann Haeusler and Valeria de Paiva, Springer, 2014, pp. 1–29.

(iv) Reference for D'Agostino's ND:
Marcello D’Agostino   Classical Natural Deduction. In: We Will Show Them! (1)  Edited by: Sergei N Artëmov, Howard Barringer, Artur S d’Avila Garcez, Luís C Lamb, John Woods.   429-468 College Publications isbn: 1-904987-11-7, (2005).