[Agda] An article by Jean-Yves Girard

Xuanrui Qi xuanrui at nagoya-u.jp
Tue Apr 21 14:54:56 CEST 2020 

> 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.

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

More information about the Agda mailing list