Popular lecture on mathematical logic

Question

Background:

I am to hold a short (10-15 min) talk that is supposed to inspire first-year undergraduate students to (in the future) take on courses in mathematical logic. They have only been introduced to the very basics of propositional logic. An obvious candidate would be Gödel's incompleteness theorems, but there is already so much accessible material produced on this topic, so I would rather choose something else. I have considered something on the arithmetical hierarchy, but I find it difficult to point to a result in this topic that is mindblowing in the same sense as Gödel's theorems are.

Furthermore, I think it would be especially nice to introduce them to some topic in constructive mathematics. I have considered explaining why the seemingly controversial statement every function on the reals is continuous is not as crazy as it sounds. I'm thinking that perhaps this should catch their attention.

Question(s):

To summarise i have three questions (independent of each other)

1. Are there any other counterintuitive results in general mathematical logic that you think would be met with as much enthusiasm as I believe that Gödel's incompleteness theorems would be (sorry, I do realise that this question is somewhat vague).
2. What would be a good way to introduce the fundamental concepts of the arithmetical hierarchy in a captivating way that does not require any background in logic? Do you have any suggestions of results I can present that will both be accessible and (hopefully) interesting to a non-specialised undergraduate student.
3. Do you have any suggestions for how I can introduce the concepts and ideas behind constructive mathematics? It would be nice to include some counterintuitive result, like the one I mentioned.

Any suggestions would be very much appreciated!

EDIT: I do realise that there are thousands of threads like this, but there is little on mathematical logic in these. In any case, if this has been asked before, then I apologise in advance.

Answer 1

In Forever Undecided, Smullyan made a detour from his normal (and amazing) Gödel discussions to talk about an intuitive reframing of Löb's theorem. If you feel like your students are already familiar with Gödel, that might be something fresh for them.

Answer 2

I would suggest showing how much you can do with mathematical logic ... as a way to lead up to Godel.

Here is a good starting point: a website that lists the formal proofs that have been completed in various mathematical proof systems. You could follow some of the links and show some specific proof (I personally like Metamath's website, as all the subresults are linked, and so you get some idea as to how crazy big some of these proofs are).

In this context, you can then also take about the formalizations of the Four Color Theorem (first purely formal proof was produced in 2005), and Kepler's Sphere Packing Conjecture (formal proof completed in 2014) ... which can get into some nice discussions as to what exactly counts as a proof as well...

And, all this will then bring up the natural question: can we formalize all? ... thus Godel.

All in all, more like 30-40 minutes though .. rather than 10-15. But maybe you can polish it down to 20 minutes, Ted Talk -style

Answer 3

I know this is an old question but...

(1) An obvious candidate would be Gödel's incompleteness theorems, but there is already so much accessible material produced on this topic, so I would rather choose something else.

I actually disagree a bit with this statement, because most popular accounts of the incompleteness theorems are just too flawed to be beneficial. Also, some nice aspects are very little known, such as the generalized computability-based versions and proofs. In particular, the zero-guessing problem mentioned in that post, which I didn't learn of until reading Scott Aaronson's blog-post cited there, is in my opinion a far better way of getting the strongest result than Rosser's trick. Since your target audience is first-year mathematics majors, they would be able to easily understand the unsolvability of the halting problem and its proof, and the same goes for the zero-guessing problem.

(2) What would be a good way to introduce the fundamental concepts of the arithmetical hierarchy in a captivating way that does not require any background in logic?

FOL can be understood via game semantics. With that, every extra quantifier in the arithmetical hierarchy is simply an extra move in the game. Note that this conception is quite robust; it applies just as well to arithmetical sentences as it does to sentences about programs. A $Σ_0$/$Π_0$-sentence is roughly one that you can prove or disprove by going through all the cases; no moves are needed.

A $Σ_1$-sentence is one that the Prover makes a single move to reduce it to a $Π_0$-sentence. If it is true, then Prover can win by an explicit move. But if it is false, then the Refuter wins, but it may be that the foundational system that they both agree on is insufficient to tell them who wins, because the Prover has infinitely many possible moves. Every halting problem instance is a $Σ_1$-sentence. If a program halts on some input, you can check that it does, but if it does not halt then you may not be able to figure that out in general, no matter how strong your assumptions. Relatedly, consistency statements are all $Π_1$-sentences (and the earlier linked post explicitly shows this). And some well-known open problems are equivalent modulo mild assumptions to $Π_1$-sentences, such as Goldbach and RH.

What about a $Π_2$-sentence? The game involves Refuter making the first move and then Prover making the second and final move. Totality statements (i.e. this program halts on every input) are all $Π_2$-sentences (with the second move being to give the full program trace). Some well known open problems such as TwinPrime and Collatz and P≠NP are $Π_2$.

(3) Do you have any suggestions for how I can introduce the concepts and ideas behind constructive mathematics? It would be nice to include some counterintuitive result, like the one I mentioned.

I don't agree that "every function on $ℝ$ is continuous" is nice. It is not much different from "every function on $ℕ$ is computable". Saying wrong things about functions on $ℝ$ just for the 'shock-factor' is just wrong. It would be better to simply say:

Every computable function on computable reals is continuous. And it turns out that we can construct a formal theory for computable functions and computable reals, which involves intuitionistic logic.

Just like ACF is a formal theory for $⟨ℂ,0,1,+,·⟩$, and we should say "every complex number has a square-root" and not "every object has a square-root". The only exception is if you truly believe that there is no uncomputable function on $ℕ$, but such a belief amounts to rejecting the meaningfulness of the halting problem.