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)



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



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:,