[Agda] An article by Jean-Yves Girard

[Philippe de Rochambeau]

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 <mailto:phiroc at free.fr>> wrote:
>> Good morning,
>> interesting article by Jean-Yves Girard (in French) : https://girard.perso.math.cnrs.fr/titres.pdf <https://girard.perso.math.cnrs.fr/titres.pdf> (who inspired Hindley and others)
>> Cheers,
>> Philippe
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/agda <https://lists.chalmers.se/mailman/listinfo/agda>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200420/795335ae/attachment.html>