[Agda] An article by Jean-Yves Girard

[mechvel at scico.botik.ru]

The first trouble with this paper is that its abstract explains nothing.
It particular, it gives no comment about what is Euler-Poincaré 
Invariant.
The names of Euler and Poincare sound encouraging, but the whole 
abstract, and
the below explanation about snake, Copernical revolution, and 21-th 
century
make the reader doubt about the goal these famous names are used for.

--
SM



On 2020-04-20 20:16, Philippe de Rochambeau wrote:
> Hello,
> 
> let me translate the summary of the article written by Jean-Yves
> Girard (https://en.wikipedia.org/wiki/Jean-Yves_Girard) entitled
> "La logique 2.0"; i.e.,"Logic 2.0" (cf.
> https://girard.perso.math.cnrs.fr/logique2.0.pdf)
> and the first paragraph.
> 
> "_In this tract, I lay the foundations of a radical reinterpretation
> of logic. Which _
> _I illustrate with technical developments: in particular a notion of
> truth based_
> _on the Euler-Poincaré Invariant"._
> 
> _Introduction : the return of philosophy_
> 
> _At the end of the Nineteenth Century, Logic underwent a spectacular
> Renaissance._
> _But, just like a snake growing so fast that it didn't shed its skin,
> it's still wearing_
> _its shirt of Nessus; the scientistic form of its Founding Fathers has
> now become _
> _obsolete. "Demonstration networks" of Linear Logic have made manifest
> this obsolescence._
> _It is now time to change the framework of interpretation and to carry
> out a_
> _"Copernician Revolution" : a passage to Logic 2.0."_
> 
> I don't have time to translate the rest of the article — it’s
> 27-pages long —. But, basically, Girard is saying
> that the challenge for logicians of the 21st Century, is to combine
> Logic and Philosophy.
> 
> The full article is worth a read, if you understand French.
> 
> Best regards,
> 
> Philippe
> 
> PS I discovered Girard this morning, on the Net, after reading
> Reinhold’s article entitled « ‘Type' is not a Type: Preliminary
> Report »
> in which he quotes the former’s 1972 Ph D Thesis.
> 
>> Le 20 avr. 2020 à 09:54, Philippe de Rochambeau <phiroc at free.fr> a
>> écrit :
>> 
>> Hi Jesper,Sure.
>> I’ll summarize tonight or tomorrow.
>> Best regards,
>> Philippe
>> 
>>> Le 20 avr. 2020 à 09:20, Jesper Cockx <Jesper at sikanda.be> a
>>> écrit :
>> 
>> 
>> 
>> Hi Philippe,
>> 
>> Could you share something about the article why you think it is
>> interesting to the Agda community? Not everyone here is fluent in
>> French.
>> 
>> -- Jesper
>> 
>> On Mon, Apr 20, 2020 at 9:01 AM Philippe de Rochambeau
>> <phiroc at free.fr> wrote:
>> 
>> Good morning,
>> interesting article by Jean-Yves Girard (in French) :
>> https://girard.perso.math.cnrs.fr/titres.pdf (who inspired Hindley
>> and others)
>> Cheers,
>> Philippe_______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda