[FOM] 491:Formal Simplicity

[David Roberts]

I sent this privately to Harvey, but perhaps a public airing will be
good too (I've made small, inconsequential edits to the original).

--

Dear Harvey,

You asked about local naturalness, and how to express this. One fact
which may be worth pointing out is that your primitives work entirely
in naïve set theory, using PP(Q) or similar. Perhaps this is what you
mean by sugared set theory--it is a term I have never heard before.
Additionally, if you know that the subsets of Q involved are logically
simple, then this cuts down the full powerset to something more
manageable (and less impredicative).

The most convincing presentation of these results for me would be to
figure out which system of reverse mathematics is the minimum to state
the proposition, and then link that to 'everyday mathematics'. The
effect is largely psychological, but that may be the level of
subterfuge you need to use to get over people's objections as to the
naturalness.

Stating the result in the form 'assuming enough mathematics to prove
integrals over compact intervals exist, one has statements which are
equivalent to consistency of large cardinals' (assuming WKL_0 is the
required strength, though I vaguely recall you mention ACA'_0 at some
point). This means that as soon as we teach students elementary
calculus, we have lead them into a world which is far wilder than even
most mathematicians understand.

Best,

David