# Rome Workshop

## Rome, 21-22 May 2015

Workshop of the Joint French-German research project funded by ANR and DFG, Beyond Logic: Hypothetical Reasoning in Philosophy of Science, Informatics, and Law, in cooperation with the research Group Logica e Geometria della Cognizione, Univ. Roma Tre.

## Conference venue

### Univ. Roma Tre, Department of "Matematica e Fisica", Largo San Leonardo Murialdo 1, building C

## Speakers include:

- Cesare Cozzo (Sapienza Univ., Roma)
- Jean Fichot (IHPST, Univ. Paris 1)
- Jean-Baptiste Joinet (Univ. Lyon 3)
- Maël Pégny (IHPST, Univ. Paris 1)
- Luiz Carlos Pereira (PUC Rio)
- Thomas Piecha (Univ. Tübingen)
- Paolo Pistone (Univ. Roma Tre & Aix-Marseille)
- Peter Schroeder-Heister (Univ. Tübingen)
- Arnaud Valence (Univ. Roma Tre)

## Program

### Thursday, 21 May 2015

#### Room: Aula F

15h00 - 16h00 | Luiz Carlos Pereira (PUC Rio de Janeiro): Translations: a view from proof-theory |

16h15 - 17h15 | Cesare Cozzo (Sapienza Univ., Roma): Dummett on inference |

17h30 - 18h30 | Arnaud Valence (Univ. Roma Tre): Dewey's Logic Revisited |

20h00 | Dinner |

### Friday, 22 May 2015

#### Room: Aula 311

9h30 - 10h30 | Jean Fichot (IHPST, Univ. Paris 1): Principles(s) of conservativity |

10h45 - 11h45 | Jean-Baptiste Joinet (Univ. Lyon 3): Actional processes, individuals and identity criteria |

12h00 - 13h00 | Paolo Pistone (Univ. Roma Tre & Aix-Marseille Univ.): Untyped validity: completeness through parametricity |

13h15 | Lunch ("Sala riunioni") |

#### Room: Aula 211

15h00 - 16h00 | Maël Pégny (IHPST, Univ. Paris 1): Constructivity and the Church-Turing thesis |

16h15 - 17h15 | Thomas Piecha (Univ. Tübingen): Inversion of logical rules |

17h30 - 18h30 | Peter Schroeder-Heister (Univ. Tübingen): Proof-theoretic semantics and the sequent calculus |

20h00 | Dinner |

## Abstracts

### Cesare Cozzo (Sapienza Univ., Roma)

Dummett on inference

**Abstract:** The notion of inference plays a pivotal role in Michael Dummett's thought. In the first part of my paper I pinpoint some salient features that distinguish Dummett's conception of inference and his views on the relations between inferential practice, logical theory and the theory of meaning. In the second part I take up the problem "how can a deductive inference be both legitimate and useful?" and expound Dummett's proposed solution. The last part is reserved for some critical comments.

### Jean Fichot (IHPST, Univ. Paris 1)

Principles(s) of conservativity

**Abstract:** TBA

### Jean-Baptiste Joinet (Univ. Lyon 3)

Actional processes, individuals and identity criteria

**Abstract:** TBA

### Maël Pégny (IHPST, Univ. Paris 1)

Constructivity and the Church-Turing thesis

**Abstract:** In this presentation, I will try to show how debates on the notion of constructivity can be enlightened by recent discussions around the Church-Turing thesis. The talk will be mainly programmatic: its main aim will be to bring more general awareness of recent works on computability into the logic and philosophy of logic community, and to stir reactions on some bold conjectures on constructivity one could formulate from this 'computability' point of view.

### Luiz Carlos Pereira (PUC Rio de Janeiro)

Translations: a view from proof-theory

**Abstract:** TBA

### Thomas Piecha (Univ. Tübingen)

Inversion of logical rules

**Abstract:** We consider the sequent calculus of minimal propositional logic, where we read the left and right introduction rules as definitions of logical constants. In a framework based on definitional reflection the left introduction rules can be shown to be inverse to the right introduction rules and vice versa.

### Paolo Pistone (Univ. Roma Tre & Aix-Marseille Univ.), joint work with Mattia Petrolo (IHPST, Univ. Paris 1)

Untyped validity: completeness through parametricity

**Abstract:** Proof-theoretic validity is usually defined as a property of derivations built according to a previously defined set of rules (see e.g. Prawitz [1971]). The setting of Pure Natural Deduction, that we recently introduced, allows to define validity without reference to rules, in the style of Tait-Girard reducibility.

Pure (or "untyped") derivations reproduce the computational behavior of pure lambda-terms, including the possible violation of the normalization property (hence they allow for the representation of paradoxes).

From an intuitionist natural deduction (NJ) derivation D, a pure derivation D^- can always be obtained by deleting formulae and labels for rules.

We prove a completeness theorem of the form: if d is a valid (closed and normal) pure derivation, then d is of the form D^- for a certain NJ derivation. The proof exploits the property of parametricity (in the sense of Reynolds[1984]) for valid derivations, i.e. their implicit second order character

### Peter Schroeder-Heister (Univ. Tübingen)

Proof-theoretic semantics and the sequent calculus

**Abstract:** In proof-theoretic semantics, the central model of reasoning has been natural deduction. This is due to the fact that Gentzen, even though he carried out all his technical investigations in sequent-style formalisms, equipped natural deduction from the very beginning with a philosophical underpinning regarding the symmetry of introduction and elimination rules. This symmetry was later spelled out in detail by Prawitz in the form of an inversion principle and integrated by Dummett into an encompassing theory of meaning. However, as I have argued elsewhere, the sequent calculus has many benefits that make it superior (or at least not inferior) to natural deduction even from the philosophical side.

Here I will present some ideas that discuss the incorporation of features of natural deduction into the sequent calculus.

In particular, I discuss the consequences of a left-introduction rule different from Gentzen's that gives implication a rule-like shape, which sheds some new light on the relationship between natural deduction and sequent calculus. I also discuss the symmetry of right and left rules in the sequent calculus that use a principle related to definitional reflection.

### Arnaud Valence (Univ. Roma Tre)

Dewey’s Logic Revisited

**Abstract:** TBA

## Local organizers

V. Michele Abrusci and Paolo Pistone

Further information: http://ls.informatik.uni-tuebingen.de/bl/, http://logica.uniroma3.it