
<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="">Hello,</div><div class=""><br class=""></div><div class="">let me translate the summary of the article written by Jean-Yves</div><div class="">Girard (<a href="https://en.wikipedia.org/wiki/Jean-Yves_Girard" class="">https://en.wikipedia.org/wiki/Jean-Yves_Girard</a>) entitled</div><div class="">"La logique 2.0"; i.e.,"Logic 2.0" (cf. <a href="https://girard.perso.math.cnrs.fr/logique2.0.pdf" class="">https://girard.perso.math.cnrs.fr/logique2.0.pdf</a>)</div><div class="">and the first paragraph.</div><div class=""><br class=""></div><div class="">"<i class="">In this tract, I lay the foundations of a radical reinterpretation of logic. Which </i></div><div class=""><i class="">I illustrate with technical developments: in particular a notion of truth based</i></div><div class=""><i class="">on the Euler-Poincaré Invariant".</i></div><div class=""><i class=""><br class=""></i></div><div class=""><i class="">Introduction : the return of philosophy</i></div><div class=""><i class=""><br class=""></i></div><div class=""><i class="">At the end of the Nineteenth Century, Logic underwent a spectacular Renaissance.</i></div><div class=""><i class="">But, just like a snake growing so fast that it didn't shed its skin, it's still wearing</i></div><div class=""><i class="">its shirt of Nessus; the scientistic form of its Founding Fathers has now become </i></div><div class=""><i class="">obsolete. "Demonstration networks" of Linear Logic have made manifest this obsolescence.</i></div><div class=""><i class="">It is now time to change the framework of interpretation and to carry out a</i></div><div class=""><i class="">"Copernician Revolution" : a passage to Logic 2.0."</i></div><div class=""><br class=""></div><div class="">I don't have time to translate the rest of the article — it’s 27-pages long —. But, basically, Girard is saying</div><div class="">that the challenge for logicians of the 21st Century, is to combine Logic and Philosophy.</div><div class=""><br class=""></div><div class="">The full article is worth a read, if you understand French.</div><div class=""><br class=""></div><div class="">Best regards,</div><div class=""><br class=""></div><div class="">Philippe</div><div class=""><br class=""></div><div class="">PS I discovered Girard this morning, on the Net, after reading Reinhold’s article entitled « ‘Type' is not a Type: Preliminary Report »</div><div class="">in which he quotes the former’s 1972 Ph D Thesis.</div><div><br class=""><blockquote type="cite" class=""><div class="">Le 20 avr. 2020 à 09:54, Philippe de Rochambeau <<a href="mailto:phiroc@free.fr" class="">phiroc@free.fr</a>> a écrit :</div><br class="Apple-interchange-newline"><div class=""><meta http-equiv="content-type" content="text/html; charset=utf-8" class=""><div dir="auto" class=""><div class="">Hi Jesper,</div>Sure.<div class="">I’ll summarize tonight or tomorrow.<br class=""><div class="">Best regards,<br class=""><div dir="ltr" class="">Philippe</div><div dir="ltr" class=""><br class=""><blockquote type="cite" class="">Le 20 avr. 2020 à 09:20, Jesper Cockx <<a href="mailto:Jesper@sikanda.be" class="">Jesper@sikanda.be</a>> a écrit :<br class=""><br class=""></blockquote></div><blockquote type="cite" class=""><div dir="ltr" class=""><div dir="ltr" class=""><div class="">Hi Philippe,</div><div class=""><br class=""></div><div class="">Could you share something about the article why you think it is interesting to the Agda community? Not everyone here is fluent in French.</div><div class=""><br class=""></div><div class="">-- Jesper<br class=""></div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Apr 20, 2020 at 9:01 AM Philippe de Rochambeau <<a href="mailto:phiroc@free.fr" target="_blank" class="">phiroc@free.fr</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="">Good morning,<div class="">interesting article by Jean-Yves Girard (in French) : <a href="https://girard.perso.math.cnrs.fr/titres.pdf" target="_blank" class="">https://girard.perso.math.cnrs.fr/titres.pdf</a> (who inspired Hindley and others)</div><div class="">Cheers,</div><div class="">Philippe</div></div>_______________________________________________<br class="">

Agda mailing list<br class="">

<a href="mailto:Agda@lists.chalmers.se" target="_blank" class="">Agda@lists.chalmers.se</a><br class="">

<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="">

</blockquote></div>

</div></blockquote></div></div></div></div></blockquote></div><br class=""></body></html>