[Agda] An article by Jean-Yves Girard

Tue Apr 21 15:24:17 CEST 2020

On 2020-04-21 15:54, Xuanrui Qi wrote:
>> 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.
> 
> I'm afraid many people on this list would not agree with this
> statement. From what little I know about topos theory, many proofs can
> be greatly simplified using topos theory. Ingo Blechschmidt, for
> example, used topos theory to simplify many proofs in algebraic
> geometry [1]. Ingo himself might be on this list, so I won't say too
> much about his work. But this is a divergence.

I just transfer the opinion of a certain expert in logic who is aware of 
the topos
approach. He referred this way to a certain dissertation. This was in 
about 1995.

I am sorry, I know nothing about topos.
May be, the approach is good.
But I am sure that a true paper is not written this way.
Maybe other papers will do ...

------
Sergei

> Of course, I won't say it's a great article just because it's written
> by Jean-Yves Girard, because I can't read much French. But from a peek
> at Girard's article it looks very interesting, and somehow related to
> the synthetic view of logic as proposed by topos theory and friends.
> This view is definitely worth exploring and I'd be interested in
> understanding what Girard thinks about it.
> 
> -Xuanrui
> 
> [1]: https://rawgit.com/iblech/internal-methods/master/notes.pdf
> 
> On Tue, 2020-04-21 at 00:16 +0300, mechvel at scico.botik.ru wrote:
>> 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
>> 
>> _______________________________________________
>> 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