[Agda] An article by Jean-Yves Girard

[mechvel at scico.botik.ru]

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