[FOM] Grothendieck foundations progress, and a posted error

[Colin McLarty]

Responding to my note that the core of cohomological number theory can
be formalized in ZFC[1], Harvey Friedman
<friedman at math.ohio-state.edu> wrote:
>
> Are there any interesting issues of "necessary uses of such strong systems"
> in your contexts?

No, not so far.  Certainly nothing here suggests that FLT is not
provable in PA, or in EFA.

Overall, my impression is the opposite.  The material is very
"algebraic," in the sense of low apparent quantifier complexity;  and
the core of cohomology admits a quick uniform expression in ZFC[1].
There is every reason to think each specific application can use a
weak fragment of the general theory. .

In practical terms: for now I pursue further reductions, and only
wonder a little about evidence of some lower bound.

As to interpretability of ZF[0] in second order arithmetic:

> There is a reason why this is an elusive result.
   ....
> this
> uses quite a bit of old machinery - particularly, Goedel's L technology
> crafted for fragments of ZF.

Ah!  Thanks.  For now I will use the result without trying to prove it.

Am I right that the general idea is to interpret ZF[0] sets as trees
presented as relations in second order arithmetic, with some
definability or constructibility condition put on the trees to make
all the axioms of ZF[0] or of ZFC[0] come out true?

I will see you in a few days in Chicago.

best, Colin