Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: logic

Topic: Girard's latest work

Robin Piedeleu (Jun 17 2020 at 09:57):

Has anyone been able to interpret J.-Y. Girard's latest papers on what he calls "transcendental syntax" and, more recently, "logique 2.0"? I briefly glanced at it but my exegetic skills are no match for his notoriously difficult prose! Is he still actively collaborating or communicating with anyone that might be able to explain some of this work?

Kenji Maillard (Jun 17 2020 at 13:08):

If you read french, I found what he calls his necrology to be somewhat helpful in having an idea of what kind of logical roadmap he had in mind

Robin Piedeleu (Jun 18 2020 at 07:13):

Thanks, that's helpful. Still somewhat mystifying to me though, in particular the reduction of first-order logic to the propositional fragment, with the constants フ and ヲ. Have you been able to make sense of these more recent developments?

Amar Hadzihasanovic (Jun 18 2020 at 08:55):

I think Thomas Seiller may have had a student working on it? In that case perhaps @Nguyễn Lê Thành Dũng knows about it?

Lê Thành Dũng (Tito) Nguyễn (Jun 18 2020 at 09:49):

The student in question is Boris Eng ( https://engboris.github.io/ ). If you speak French you can look at his internship report https://engboris.github.io/documents/report_m2.pdf
(Thanks for the ping @Amar Hadzihasanovic!)

Lê Thành Dũng (Tito) Nguyễn (Jun 18 2020 at 09:51):

I've looked a bit at this stuff myself; I recall that in 2018 I attended an informal workshop organized by Thomas Seiller and Paolo Pistone on transcendental syntax. But we didn't really manage to understand the logic 2.0 stuff. (Girard himself was also invited to answer our questions, but instead he went on a lot of tangents, of the usual kind such as "Tarski was stupid and Russell was a eugenicist".)

Lê Thành Dũng (Tito) Nguyễn (Jun 18 2020 at 09:53):

Anyway, Boris's internship was about giving clean definition and proofs for the "semantics of MLL using stars and constellations" part, but it didn't cover the first-order logic part; I think the latter is one of his eventual goals with Thomas.

Lê Thành Dũng (Tito) Nguyễn (Jun 18 2020 at 10:01):

As for フ and ヲ, the idea is supposed to be the following I think: there are only two "stars" (generalized proof nets), up to isomorphism, with a single atomic conclusion; one of them is "objective" and the other is "subjective" (which I think is an attribute you can arbitrarily set for some conclusions of a star). フ and ヲare maybe the singleton sets containing those respective stars (types should be ultimately sets of stars, I think?).

Amar Hadzihasanovic (Jun 18 2020 at 10:09):

Thanks, that's brilliant! Now I just have to resist the temptation of reading it instead of working on my paper.

Robin Piedeleu (Jun 18 2020 at 12:27):

Thanks a lot, @Nguyễn Lê Thành Dũng! The distinction between "objective" and "subjective" proofs/stars sounds interesting.

Robin Piedeleu (Jun 18 2020 at 12:27):

I'll have a look at Boris' report, thanks for the link.

Kenji Maillard (Jun 18 2020 at 12:56):

I stopped following the recent girardisms for a few years so I don;t have much clues about transcendental syntax and its offsprings. Boris' report is really great (not so often that a report for MPRI is that readable) but now I'm wondering quite a few basic questions about the specific encoding of stars: why are these multisets ? Could we just consider them as well as substitutions up to reordering ? why are colors encoded using function symbols in the underlying language ? Where does that language comes from to start with (like, what's specific to it) ?

Lê Thành Dũng (Tito) Nguyễn (Jun 19 2020 at 23:09):

I'm told that Boris and Thomas intend to submit something to CSL; in any case, a preprint on transcendental syntax in English should appear soon-ish.

Lê Thành Dũng (Tito) Nguyễn (Jul 09 2020 at 14:14):

And here is the paper: https://www.seiller.org/documents/articles/Stellar.pdf

Amar Hadzihasanovic (Jul 11 2020 at 12:21):

Great!
I've started reading it. There seems to be something missing in Definition 15; the multigraph they define doesn't even depend on the set $\mathcal{A}$ of colours. From the example following, my guess of the intended definition would be:
there is an edge between $(s, r)$ and $(s',r')$ if $r = -c(t_1, \ldots, t_n)$, $r' = +c(t'_1, \ldots, t'_n)$, $c \in \mathcal{A}$, and $c(t_1, \ldots, t_n)$ and $c(t'_1, \ldots, t'_n)$ are matchable...

Thomas Seiller (Jul 15 2020 at 21:26):

@Amar Hadzihasanovic Your guess is right :-), but I initially wrote the definition in two steps (defining “dual rays” wrt a set of colours, and then replacing “matchable” by dual wrt A in definition 15). I do no know how it ended up this way.
I’ll fix that as soon as I get my hands on my computer (this will take a few days).