Talk - Why Think -- Letting Computers do Math for Us

23 Jan 2021 - Tags: my-talks

Yesterday I gave my second talk at the Graduate Student Seminar at UCR. I decided to talk about something near and dear to me, a topic which first got me interested in logic: decidability. The idea of decidability is to look for theories which are simple enough to admit a computer program (called a decider) which can tell you whether or not a given sentence is true.

I was first introduced to the decidability of certain logics in Computational Discrete Math (CDM) which was the class where I met my advisor Klaus Sutner. I’m lazy at times, and so the idea of a decidable logic was really exciting. I wanted to know as much as I could so that, one day, I would be able to answer a tricky question by asking a computer!

Of course, now I realize that a lot of the time it’s faster to just solve the problem yourself than ask a decider (particularly if you have to write the decider yourself…) but the interest has stuck with me. I think it’s a super cool topic, and I was really pleased to get a chance to talk at length about it!

There are a ton of decidability results in logic, but only an hour in a talk. Also, a lot of the techniques for proving decidability are somewhat technical. This made drafting the talk a little bit tricky, particularly since I was speaking to a room of non-logicians. The best bet, I thought, was to try and survey a few powerful techniques (completeness and automaticity) and give a high level description of how the proofs go. Then I ended with a discussion of some negative results, and a tangent on the resolution of Hilbert’s 10th Problem. It’s not directly related, but Matiyasevich’s Theorem was my favorite theorem for a while, and the material was so nearby that I couldn’t resist including it!

All in all, I think the talk went quite well ^_^. Klaus is (among other things) an Automata Theorist, and working closely with him for a few years made me love automata too. I was happy to get to share some of that enthusiasm with people, even if I had to gloss over some details. Plus, I’m really proud of the example computation done on an automaton. I made it with Evan Wallace’s FSM Maker and then tweaked the tikz slide by slide to do the animation. Normally I would draw the machine on a blackboard and point at the current state, but I think the colors served as a nice substitute for a talk with slides.

I had someone ask me how the automatic structure is useful in deciding a theory, and in hindsight I should have included a slide on that. I’m glad they asked, though, because it gave me a chance to describe it verbally. That’s a really obvious oversight, and I’m a bit upset that people who only download the slides won’t get a chance to see an overview of that proof. Maybe I’ll write it up in a blog post one day and include a simple example…

As for the other material, it’s always harder to tell over zoom, but I think people followed the talk fairly well. The section on completeness was necessarily a bit technical, and I’m almost certain I lost some people in the proof that $\mathsf{DLO}$ has Quantifier Elimination. That said, I expected to lose some people there (it’s not an obvious bit of combinatorics, even if it’s easy once you’re familiar with it), so I’m not too upset about it. The point of that slide was to show that Quantifier Elimination is a strategy for getting control over your favorite theory. If anyone ever needs it for their research, they’ll have plenty of time to look for it and learn it themselves now that they know it exists.

As one last regret for the road, someone asked where people are studying these questions. I threw out Cornell and UIUC as guesses, but in hindsight I don’t think I made it clear that I don’t actually know for certain that people there are working on this stuff. I said that in any good logic department you’ll have people interested in these things, and that’s true, but I don’t actually know if there’s anyone explicitly doing work in this area. Also, I should have probably plugged CMU…

As always, the abstract and slides are below. Plus a link to a youtube video¹ with a recording of the talk.

---

Why Think? Letting Computers Do Math For Us

There are a number of results in logic of the form “If your question can be asked a certain way, then there is an algorithm which tells you the answer”. These are called Decidability Theorems, because an algorithm can Decide if a proposition is true or false. In this talk we will survey some results in this area, discuss a few techniques for proving these results, and discuss some open problems are only a few computer cycles away from being solved.

The talk slides are here. There’s at least one minor typo (I say Łoś-Tarski at one point when I mean Łoś-Vaught)

A recording of the talk is embedded below.

---