
<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body dir="auto">Hi,<div>It has to do with proving truths, but don’t ask me to explain how or why:</div><div>I’ve found three articles written by Girard in English on the Google Scholar Website which seem to go into details:</div><div><br></div><div><a href="https://scholar.google.fr/scholar?q=Transcendental+syntax+3+:+equality.+Logical+Methods+in+Computer+Science,+2016&hl=fr&as_sdt=0&as_vis=1&oi=scholart">https://scholar.google.fr/scholar?q=Transcendental+syntax+3+:+equality.+Logical+Methods+in+Computer+Science,+2016&hl=fr&as_sdt=0&as_vis=1&oi=scholart</a></div><div><div><div><div><br><div dir="ltr">Philippe</div><div dir="ltr"><br><blockquote type="cite">Le 20 avr. 2020 à 20:21, mechvel@scico.botik.ru a écrit :<br><br></blockquote></div><blockquote type="cite"><div dir="ltr"><span>This invariant parobably has a relevance to the Euler equality relating</span><br><span>the number sides, edges and vertices in a polyghon in a three-dimensional</span><br><span>space. Something of this sort.</span><br><span>But the abstract and introduction take a great effort to hide its relevance</span><br><span>to logic (if there is any relevance).</span><br><span></span><br><span></span><br><span>On 2020-04-20 21:00, mechvel@scico.botik.ru wrote:</span><br><blockquote type="cite"><span>The first trouble with this paper is that its abstract explains nothing.</span><br></blockquote><blockquote type="cite"><span>It particular, it gives no comment about what is Euler-Poincaré Invariant.</span><br></blockquote><blockquote type="cite"><span>The names of Euler and Poincare sound encouraging, but the whole abstract, and</span><br></blockquote><blockquote type="cite"><span>the below explanation about snake, Copernical revolution, and 21-th century</span><br></blockquote><blockquote type="cite"><span>make the reader doubt about the goal these famous names are used for.</span><br></blockquote><blockquote type="cite"><span>--</span><br></blockquote><blockquote type="cite"><span>SM</span><br></blockquote><blockquote type="cite"><span>On 2020-04-20 20:16, Philippe de Rochambeau wrote:</span><br></blockquote><blockquote type="cite"><blockquote type="cite"><span>Hello,</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>let me translate the summary of the article written by Jean-Yves</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Girard (https://en.wikipedia.org/wiki/Jean-Yves_Girard) entitled</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>"La logique 2.0"; i.e.,"Logic 2.0" (cf.</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>https://girard.perso.math.cnrs.fr/logique2.0.pdf)</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>and the first paragraph.</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>"_In this tract, I lay the foundations of a radical reinterpretation</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>of logic. Which _</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>_I illustrate with technical developments: in particular a notion of</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>truth based_</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>_on the Euler-Poincaré Invariant"._</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>_Introduction : the return of philosophy_</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>_At the end of the Nineteenth Century, Logic underwent a spectacular</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Renaissance._</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>_But, just like a snake growing so fast that it didn't shed its skin,</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>it's still wearing_</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>_its shirt of Nessus; the scientistic form of its Founding Fathers has</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>now become _</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>_obsolete. "Demonstration networks" of Linear Logic have made manifest</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>this obsolescence._</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>_It is now time to change the framework of interpretation and to carry</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>out a_</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>_"Copernician Revolution" : a passage to Logic 2.0."_</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>I don't have time to translate the rest of the article — it’s</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>27-pages long —. But, basically, Girard is saying</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>that the challenge for logicians of the 21st Century, is to combine</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Logic and Philosophy.</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>The full article is worth a read, if you understand French.</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Best regards,</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Philippe</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>PS I discovered Girard this morning, on the Net, after reading</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Reinhold’s article entitled « ‘Type' is not a Type: Preliminary</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Report »</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>in which he quotes the former’s 1972 Ph D Thesis.</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Le 20 avr. 2020 à 09:54, Philippe de Rochambeau <phiroc@free.fr> a</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>écrit :</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Hi Jesper,Sure.</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>I’ll summarize tonight or tomorrow.</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Best regards,</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Philippe</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Le 20 avr. 2020 à 09:20, Jesper Cockx <Jesper@sikanda.be> a</span><br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>écrit :</span><br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span></span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Hi Philippe,</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Could you share something about the article why you think it is</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>interesting to the Agda community? Not everyone here is fluent in</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>French.</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>-- Jesper</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>On Mon, Apr 20, 2020 at 9:01 AM Philippe de Rochambeau</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span><phiroc@free.fr> wrote:</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Good morning,</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>interesting article by Jean-Yves Girard (in French) :</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>https://girard.perso.math.cnrs.fr/titres.pdf (who inspired Hindley</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>and others)</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Cheers,</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Philippe_______________________________________________</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Agda mailing list</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Agda@lists.chalmers.se</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>https://lists.chalmers.se/mailman/listinfo/agda</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>_______________________________________________</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Agda mailing list</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Agda@lists.chalmers.se</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>https://lists.chalmers.se/mailman/listinfo/agda</span><br></blockquote></blockquote><blockquote type="cite"><span>_______________________________________________</span><br></blockquote><blockquote type="cite"><span>Agda mailing list</span><br></blockquote><blockquote type="cite"><span>Agda@lists.chalmers.se</span><br></blockquote><blockquote type="cite"><span>https://lists.chalmers.se/mailman/listinfo/agda</span><br></blockquote><span></span><br></div></blockquote></div></div></div></div></body></html>