Today I lectured about the Hydra game by Laurence Kirby and Jeff Paris (Accessible Independence Results for Peano Arithmetic, Kirby and Paris, Bull. London Math. Soc. 1982; 14: 285-293). For the occasion I implemented the game in Java. I am publishing the code for anyone who wants to play, or use it for teaching. (more…)
Recently there has been a discussion (here, here, here, and here) on the Foundations of Mathematics mailing list about completeness of Peano arithmetic (PA) with respect to “small” sentences. Harvey Friedman made several conjectures of the following kind: “All true small sentences of PA are provable.” He proposed measures of smallness, such as counting the number of distinct variables or restricting the depth of terms. Here are some statistics concerning such statements.
I recently lectured at an EST training workshop in Fischbachau, Germany. There were also a number of student talks, one of which was given by Luca Chiarabini from Munich. He talked about extraction of programs from proofs, using (a variant of) Curry-Howard isomorphism, also known as propositions-as-types. He had some very interesting ideas which were obviously related to old programming tricks, but he approached them from the logical point of view, rather than the programmer’s point of view. It got me thinking about how to write certain recursive programs as proofs. Since it is a nice application of program extraction, I want to share it with you here.
In constructive mathematics even very small sets can be quite a bit more interesting than in classical mathematics. Since you will not believe me that sets with at most one element are very interesting, let us look at the set of truth values, which has “two” elements.
Powered by WordPress