[Agda] An article by Jean-Yves Girard

[mechvel at scico.botik.ru]

May be, this is related to the following theorem in geometry:
each smooth orientable surface in a three-dimensional space
is topologically equal to a sphere with several handles.
So that the number of these handles is preserved under invertible 
continuous
transformations. May be this is called Euler - Poicare invariant
(?).
For example, a sphere with one handle is equivalent to torus.
Anyway the relevance of this subject to logic is hidden under the two 
famous names,
Copernic, 21-th century, a snake, and such.

In fact, 21-th century is not so particularly impressive and important.
Do we understand of what has been developed 19-th century?
How much people (even mathematicians) understand of what precisely have 
invented
Gauss, Laplace, Galois, Lobachevsky?
For example, many people think that Lobachevsky has discovered that 
parallel straight
lines can intersect, that this is the essence of the invention.

--
SM



On 2020-04-20 21:21, mechvel at scico.botik.ru wrote:
> 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