[Agda] An article by Jean-Yves Girard

[Philippe de Rochambeau]

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

Philippe

> 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
> 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200420/90d585a8/attachment.html>