brief description of our project

Here's the brief description of the baby multi-author project we are doing. There are dozens of simple unprovable statements known already: PH, KM, Kruskal, GMT, hydras, etc etc etc. Most of them, at least the simple and interesting ones are of the Pi_2 form, that is some "for all" quantifiers followed by some "exists" quantifiers followed by a formula without unbounded quantifiers. Now, MDRP theorem gives us an explicit translation of  every Sigma_1 formula, say phi(y_1, y_2, ... y_m)  into the... read more