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: community: events

Topic: Computational Logic and Applications 2020

Noam Zeilberger (Sep 03 2020 at 16:40):

Members of this community with an interest in combinatorics may be interested in CLA (https://cla.tcs.uj.edu.pl/), which is an annual interdisciplinary workshop around combinatorial and quantitative aspects of mathematical logic. This year we are going fully virtual, with CLA 2020 being held online 12-13 October. We are still accepting talk proposals, and applied category theory talks within the scope of the workshop would be most welcome. (Note the submission deadline is pretty soon: Sep 7th anytime-on-earth.) In any case, registration is free and all are welcome to participate.

Noam Zeilberger (Oct 05 2020 at 07:58):

The full programme of the CLA workshop is now online (https://cla.tcs.uj.edu.pl/#program), including 12 technical talks (see below) and an problem session, as well as a brief history of CLA by Pierre Lescanne and Marek Zaionc. If you are interested in attending any of these, please register for the workshop this week.

Invited speakers

• Mirai Ikebuchi (Massachusetts Institute of Technology), Homological Methods in Rewriting
• Marc Noy (Universitat Politècnica de Catalunya), Limiting probabilities of first order sentences in sparse random graphs

Contributed talks

• Maciej Bendkowski, A note on the asymptotic expressiveness of ZF and ZFC
• Olivier Bodini, Alexandros Singh and Noam Zeilberger, Distribution of Parameters in Certain Fragments of the Linear and Planar λ-calculus
• Antoine Genitrini, Reduced Ordered Binary Decision Diagrams as compacted tree-structures: Enumeration and Sampling
• Katarzyna Grygiel and Guan-Ru Yu, In search of a bijection between β-normal 3-indecomposable planar lambda terms and β(0,1)-trees
• Michaël Moortgat, The Tamari order for D3 and derivability in semi-associative Lambek-Grishin Calculus
• Martin Pépin, Statistical Analysis of Non-Deterministic Fork-Join Processes
• Andrew Elvey Price, Wenjie Fang and Michael Wallner, Compacted binary trees admit stretched exponentials
• Ryoma Sin'Ya, A quantitative approach to the primitive words conjecture
• Richard Statman, Algebraic and combinatorial structures intrinsic to functional programming
• Paul Tarau and Valeria de Paiva, Training Neural Networks as Theorem Provers via the Curry-Howard Isomorphism

John Baez (Oct 05 2020 at 15:52):

I wonder what Ikebuchi has to say about homological methods in rewriting... is this connected to Craig Squier's result? Oh, I guess it is.

John Baez (Oct 05 2020 at 15:52):

I also wonder what "the asymptotic expressiveness of ZF and ZFC" means.

Antonin Delpeuch (Oct 05 2020 at 17:13):

Thanks for noticing that @John Baez, I find Squier's results fascinating so I'd love to hear more about that line of work. @Noam Zeilberger, will talks be recorded?

Noam Zeilberger (Oct 05 2020 at 19:18):

@John Baez You can find abstracts for all the talks on the webpage, e.g., for Bendkowski's talk ("asymptotic expressiveness" is referring to relative asymptotic density of provable formulas among all formulas of a given size). @Antonin Delpeuch Yes the talks will be recorded! We plan to make them available sometime after the workshop.

John Baez (Oct 05 2020 at 20:24):

Thanks! That abstract is really interesting, but I'm wondering if it contains typo or something. He writes:

Secondly, we show that it is not possible to refute the existence of μ(ZFC ) within ZFC itself. For that purpose we link the provable existence of μ(ZFC) with the provable consistency of ZFC. In light of Gödel’s second incompleteness theorem, the existence of μ(ZFC) becomes unprovable within ZFC.

First he talks about "refuting the existence", and then he switches to "proving the existence".

(μ(ZFC ) is the limiting density of statements in the language of ZFC that are provable within ZFC.)

John Baez (Oct 05 2020 at 20:25):

I should probably read a paper by him to see if he's claiming the existence of μ(ZFC) cannot be proved within ZFC, cannot be refuted within ZFC, or both.

John Baez (Oct 05 2020 at 20:27):

In the abstract he says "Furthermore, we show that if ZFC consistent, it is not possible to refute the existence of the asymptotic density of ZFC theorems within ZFC itself." So there it's about refuting, not proving.

John Baez (Oct 05 2020 at 20:28):

I don't see a paper by him that discusses this. It's interesting stuff!

Noam Zeilberger (Oct 06 2020 at 07:43):

I asked Benkowski about this, here is his response:

Ohh.. that's an excellent catch! Please thank John Baez for me.
Indeed, that's an unfortunate mistake in the abstract. The revised abstract would be:

"We investigate the asymptotic densities of theorems provable in Zermelo-Fraenkel
set theory zf and its extension zfc including the axiom of choice. Assuming a canonical De
Bruijn representation of formulae, we construct asymptotically large sets of sentences unprovable
within zf, yet provable in zfc. Furthermore, we link the asymptotic density of
zfc theorems with the provable consistency of zfc itself. Consequently, if zfc is consistent, it
is not possible to refute the existence of the asymptotic density of zfc theorems within zfc.
Both these results address a recent question by Zaionc regarding the asymptotic equivalence of
zf and its extension zfc."

The mistake comes from the fact that the "link" I mention, technically speaking, means
ZFC |- ZFC is consistent iff \neg \mu(1). In the revised abstract I now mention that
I link the asymptotic density of theorems of zfc with its consistency, without specifying
any more details of that link. I hope that clarifies things now.

Noam Zeilberger (Oct 06 2020 at 07:43):

He also says, "The paper's coming soon, I need to polish some rough edges, but I hope to publish it on arxiv this week."

Morgan Rogers (he/him) (Oct 06 2020 at 08:26):

Ah, "this week", how many times I have erroneously claimed to reach that proximity to article publication...

John Baez (Oct 06 2020 at 16:35):

Great, I'm glad the abstract is clear now! It looks interesting.