License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2013.11
URN: urn:nbn:de:0030-drops-41852
Go to the corresponding LIPIcs Volume Portal

Girard, Jean-Yves

Three lightings of logic (Invited Talk)

5.pdf (0.5 MB)


Whether we deal with foundations or computation, logic relates questions and answers, typically formulas and proofs: a very entangled relation due to the abuse of presuppositions.
In order to analyse syntax, we should step out from language, which is quite impossible. However, it is enough to step out from meaning: this is why our first lighting of logic is that of answers: it is possible to deal with them as meaningless artifacts assuming two basic states, implicit and explicit. The process of explicitation (a.k.a. normalisation, execution), which aims at making explicit what is only implicit, is fundamentally hazardous.
The second light is that of questions whose choice involves a formatting ensuring the convergence of explicitation, i.e., the existence of "normal forms". This formatting can be seen as the emergence of meaning. It is indeed a necessary nuisance; either too laxist or too coercitive, there is no just format. Logic should avoid the pitfall of Prussian, axiomatic, formats by trying to understand which deontic dialogue is hidden behind logical restrictions.
The third lighting, certainty deals with the adequation between answers and questions: how do we know that an answer actually matches a question? Apodictic certainty -- beyond a reasonable doubt -- is out of reach: we can only hope for epidictic, i.e., limited, reasonable, certainty. Under the second light (questions), we see that the format is made of two opposite parts, namely rights and duties, and that logical deduction relies on a strict balance between these two opposite terms, expressed by the identity group "A is A and conversely". The issue of certainty thus becomes the interrogation: "Can we afford the rights of our duties?"

BibTeX - Entry

  author =	{Jean-Yves Girard},
  title =	{{Three lightings of logic (Invited Talk)}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{11--23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Simona Ronchi Della Rocca},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-41852},
  doi =		{10.4230/LIPIcs.CSL.2013.11},
  annote =	{Keywords: Proof theory}

Keywords: Proof theory
Collection: Computer Science Logic 2013 (CSL 2013)
Issue Date: 2013
Date of publication: 02.09.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI