<div dir='auto'><div>Hi Xuanri,<div dir="auto"><div dir="auto"><div dir="auto"><div dir="auto">Yesterday, I provided URLs pointing to articles on the Google Scolar Website which Girard wrote in English, if you are interested. I have PDF copies of parts I, II and III and parts IV, if you need them.</div></div></div></div><br><div class="gmail_extra"><br><div class="gmail_quote">Le 21 avr. 2020 14:54, Xuanrui Qi <xuanrui@nagoya-u.jp> a écrit :<br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">> The result was that simple notions<br>
> and proofs were reformulated in a complex way, and the proofs have <br>
> become many times larger and many times more complex.</p>
<p dir="ltr">I'm afraid many people on this list would not agree with this<br>
statement. From what little I know about topos theory, many proofs can<br>
be greatly simplified using topos theory. Ingo Blechschmidt, for<br>
example, used topos theory to simplify many proofs in algebraic<br>
geometry [1]. Ingo himself might be on this list, so I won't say too<br>
much about his work. But this is a divergence.</p>
<p dir="ltr">Of course, I won't say it's a great article just because it's written<br>
by Jean-Yves Girard, because I can't read much French. But from a peek<br>
at Girard's article it looks very interesting, and somehow related to<br>
the synthetic view of logic as proposed by topos theory and friends.<br>
This view is definitely worth exploring and I'd be interested in<br>
understanding what Girard thinks about it.</p>
<p dir="ltr">-Xuanrui</p>
<p dir="ltr">[1]: https://rawgit.com/iblech/internal-methods/master/notes.pdf </p>
<p dir="ltr">On Tue, 2020-04-21 at 00:16 +0300, mechvel@scico.botik.ru wrote:<br>
> Collecting all my amateur fantasy, I imagine that a logical statement<br>
> is<br>
> represented by a smooth surface, being considered modulo certain <br>
> continuous<br>
> transformations of the space. When this surface is converted to a <br>
> sphere,<br>
> the statement is proved. Something of this sort. This is like solving<br>
> a <br>
> knot<br>
> by transforming it to a trivial knot. And if the surface has at<br>
> least <br>
> one handle<br>
> (a certain topological invariant, something about Euler and<br>
> Poincare),<br>
> then it cannot be transformed to a sphere.<br>
> May be this is the idea?<br>
> <br>
> I recall that some people studied the subject of Topos - an approach<br>
> to <br>
> topology<br>
> (may be to logic also?) via the category theory. The result was that <br>
> simple notions<br>
> and proofs were reformulated in a complex way, and the proofs have <br>
> become many times<br>
> larger and many times more complex.<br>
> <br>
> If the paper aims at hiding such an effect, then indeed, it needs to <br>
> write possibly<br>
> more about Copernic, 21-th century, and a snake doing something wise <br>
> with its skin.<br>
> <br>
> --<br>
> SM<br>
> <br>
> <br>
> <br>
> On 2020-04-20 23:04, mechvel@scico.botik.ru wrote:<br>
> > On 2020-04-20 22:27, Philippe de Rochambeau wrote:<br>
> > > Hi,<br>
> > > It has to do with proving truths, but don’t ask me to explain how<br>
> > > or<br>
> > > why:<br>
> > > I’ve found three articles written by Girard in English on the<br>
> > > Google<br>
> > > Scholar Website which seem to go into details:<br>
> > > <br>
> > > 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<br>
> > <br>
> > <br>
> > The matter is that when an article is true, the author takes care<br>
> > to<br>
> > give enough hints<br>
> > in abstract and in the first page of introduction. So that to make<br>
> > the<br>
> > essence may be 1/5<br>
> > clear to the reader, to give him a hope.<br>
> > And nothing of this sorts happens there. Instead the author<br>
> > irritates<br>
> > the reader with<br>
> > reasoning about Copernic, 21-th century, and a certain snake.<br>
> > So that it is more than 99% that this is a fake.<br>
> > <br>
> > ------<br>
> > Sergei<br>
> > <br>
> > <br>
> > <br>
> > > > Le 20 avr. 2020 à 20:21, mechvel@scico.botik.ru a écrit :<br>
> > > > This invariant parobably has a relevance to the Euler equality<br>
> > > > relating<br>
> > > > the number sides, edges and vertices in a polyghon in a<br>
> > > > three-dimensional<br>
> > > > space. Something of this sort.<br>
> > > > But the abstract and introduction take a great effort to hide<br>
> > > > its<br>
> > > > relevance<br>
> > > > to logic (if there is any relevance).<br>
> > > > <br>
> > > > On 2020-04-20 21:00, mechvel@scico.botik.ru wrote:<br>
> > > > <br>
> > > > > The first trouble with this paper is that its abstract<br>
> > > > > explains<br>
> > > > > nothing.<br>
> > > > > It particular, it gives no comment about what is Euler-<br>
> > > > > Poincaré<br>
> > > > > Invariant.<br>
> > > > > The names of Euler and Poincare sound encouraging, but the<br>
> > > > > whole<br>
> > > > > abstract, and<br>
> > > > > the below explanation about snake, Copernical revolution, and<br>
> > > > > 21-th century<br>
> > > > > make the reader doubt about the goal these famous names are<br>
> > > > > used<br>
> > > > > for.<br>
> > > > > --<br>
> > > > > SM<br>
> > > > > On 2020-04-20 20:16, Philippe de Rochambeau wrote:<br>
> > > > Hello,<br>
> > > > > let me translate the summary of the article written by Jean-<br>
> > > > > Yves<br>
> > > > > Girard (https://en.wikipedia.org/wiki/Jean-Yves_Girard)<br>
> > > > > entitled<br>
> > > > > "La logique 2.0"; i.e.,"Logic 2.0" (cf.<br>
> > > > > https://girard.perso.math.cnrs.fr/logique2.0.pdf)<br>
> > > > > and the first paragraph.<br>
> > > > > "_In this tract, I lay the foundations of a radical<br>
> > > > > reinterpretation<br>
> > > > > of logic. Which _<br>
> > > > > _I illustrate with technical developments: in particular a<br>
> > > > > notion<br>
> > > > > of<br>
> > > > > truth based_<br>
> > > > > _on the Euler-Poincaré Invariant"._<br>
> > > > > _Introduction : the return of philosophy_<br>
> > > > > _At the end of the Nineteenth Century, Logic underwent a<br>
> > > > > spectacular<br>
> > > > > Renaissance._<br>
> > > > > _But, just like a snake growing so fast that it didn't shed<br>
> > > > > its<br>
> > > > > skin,<br>
> > > > > it's still wearing_<br>
> > > > > _its shirt of Nessus; the scientistic form of its Founding<br>
> > > > > Fathers<br>
> > > > > has<br>
> > > > > now become _<br>
> > > > > _obsolete. "Demonstration networks" of Linear Logic have made<br>
> > > > > manifest<br>
> > > > > this obsolescence._<br>
> > > > > _It is now time to change the framework of interpretation and<br>
> > > > > to<br>
> > > > > carry<br>
> > > > > out a_<br>
> > > > > _"Copernician Revolution" : a passage to Logic 2.0."_<br>
> > > > > I don't have time to translate the rest of the article — it’s<br>
> > > > > 27-pages long —. But, basically, Girard is saying<br>
> > > > > that the challenge for logicians of the 21st Century, is to<br>
> > > > > combine<br>
> > > > > Logic and Philosophy.<br>
> > > > > The full article is worth a read, if you understand French.<br>
> > > > > Best regards,<br>
> > > > > Philippe<br>
> > > > > PS I discovered Girard this morning, on the Net, after<br>
> > > > > reading<br>
> > > > > Reinhold’s article entitled « ‘Type' is not a Type:<br>
> > > > > Preliminary<br>
> > > > > Report »<br>
> > > > > in which he quotes the former’s 1972 Ph D Thesis.<br>
> > > > Le 20 avr. 2020 à 09:54, Philippe de Rochambeau <phiroc@free.fr<br>
> > > > > a<br>
> > > > écrit :<br>
> > > > Hi Jesper,Sure.<br>
> > > > I’ll summarize tonight or tomorrow.<br>
> > > > Best regards,<br>
> > > > Philippe<br>
> > > > Le 20 avr. 2020 à 09:20, Jesper Cockx <Jesper@sikanda.be> a<br>
> > > > écrit :<br>
> > > > <br>
> > > > Hi Philippe,<br>
> > > > Could you share something about the article why you think it is<br>
> > > > interesting to the Agda community? Not everyone here is fluent<br>
> > > > in<br>
> > > > French.<br>
> > > > -- Jesper<br>
> > > > On Mon, Apr 20, 2020 at 9:01 AM Philippe de Rochambeau<br>
> > > > <phiroc@free.fr> wrote:<br>
> > > > Good morning,<br>
> > > > interesting article by Jean-Yves Girard (in French) :<br>
> > > > https://girard.perso.math.cnrs.fr/titres.pdf (who inspired<br>
> > > > Hindley<br>
> > > > and others)<br>
> > > > Cheers,<br>
> > > > Philippe_______________________________________________<br>
> > > > Agda mailing list<br>
> > > > Agda@lists.chalmers.se<br>
> > > > https://lists.chalmers.se/mailman/listinfo/agda<br>
> > > > > _______________________________________________<br>
> > > > > Agda mailing list<br>
> > > > > Agda@lists.chalmers.se<br>
> > > > > https://lists.chalmers.se/mailman/listinfo/agda<br>
> > > > _______________________________________________<br>
> > > > Agda mailing list<br>
> > > > Agda@lists.chalmers.se<br>
> > > > https://lists.chalmers.se/mailman/listinfo/agda<br>
> > <br>
> > _______________________________________________<br>
> > Agda mailing list<br>
> > Agda@lists.chalmers.se<br>
> > https://lists.chalmers.se/mailman/listinfo/agda<br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> Agda@lists.chalmers.se<br>
> https://lists.chalmers.se/mailman/listinfo/agda</p>
<p dir="ltr">_______________________________________________<br>
Agda mailing list<br>
Agda@lists.chalmers.se<br>
https://lists.chalmers.se/mailman/listinfo/agda<br>
</p>
</blockquote></div><br></div></div></div>