[Agda] An article by Jean-Yves Girard

Tue Apr 21 00:51:20 CEST 2020

>
> The matter is that when an article is true, the author takes care to
> give enough hints
> in abstract and in the first page of introduction. So that to make the
> essence may be 1/5
> clear to the reader, to give him a hope.
> And nothing of this sorts happens there. Instead the author irritates
> the reader with
> reasoning about Copernic, 21-th century, and a certain snake.
> So that it is more than 99% that this is a fake.

But one should not forget that J.-Y. Girard is renowned inventor of the
Mustard Watch. Go well, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On Mon, 20 Apr 2020 at 17:04, <mechvel at scico.botik.ru> wrote:

> On 2020-04-20 22:27, Philippe de Rochambeau wrote:
> > Hi,
> > It has to do with proving truths, but don’t ask me to explain how or
> > why:
> > I’ve found three articles written by Girard in English on the Google
> > Scholar Website which seem to go into details:
> >
> >
> 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
>
>
>
> The matter is that when an article is true, the author takes care to
> give enough hints
> in abstract and in the first page of introduction. So that to make the
> essence may be 1/5
> clear to the reader, to give him a hope.
> And nothing of this sorts happens there. Instead the author irritates
> the reader with
> reasoning about Copernic, 21-th century, and a certain snake.
> So that it is more than 99% that this is a fake.
>
> ------
> Sergei
>
>
>
> >
> >> Le 20 avr. 2020 à 20:21, mechvel at scico.botik.ru a écrit :
> >
> >> This invariant parobably has a relevance to the Euler equality
> >> relating
> >> the number sides, edges and vertices in a polyghon in a
> >> three-dimensional
> >> space. Something of this sort.
> >> But the abstract and introduction take a great effort to hide its
> >> relevance
> >> to logic (if there is any relevance).
> >>
> >> On 2020-04-20 21:00, mechvel at scico.botik.ru wrote:
> >>
> >>> 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
> >
> >> _______________________________________________
> >
> >> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200420/a376218e/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200420/a376218e/attachment.ksh>