[Agda] An article by Jean-Yves Girard

Mon Apr 20 23:16:21 CEST 2020

Collecting all my amateur fantasy, I imagine that a logical statement is
represented by a smooth surface, being considered modulo certain 
continuous
transformations of the space. When this surface is converted to a 
sphere,
the statement is proved. Something of this sort. This is like solving a 
knot
by transforming it to a trivial knot. And if the surface has at least 
one handle
(a certain topological invariant, something about Euler and Poincare),
then it cannot be transformed to a sphere.
May be this is the idea?

I recall that some people studied the subject of Topos - an approach to 
topology
(may be to logic also?) via the category theory. The result was that 
simple notions
and proofs were reformulated in a complex way, and the proofs have 
become many times
larger and many times more complex.

If the paper aims at hiding such an effect, then indeed, it needs to 
write possibly
more about Copernic, 21-th century, and a snake doing something wise 
with its skin.

--
SM

On 2020-04-20 23: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