[Agda] An article by Jean-Yves Girard

[mechvel at scico.botik.ru]

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