FOM: HA/PA, categorical (pseudo) foundations

[Harvey Friedman]

Some of you wondered where I went, but I have big plans to get back into
the fom on a regular basis - and talk overwhelmingly about topics other
than category theory and general intellectual interest. I won't swear off
completely from these two topics - after all, Lou and Colin are still
subscribers. (By the way, why don't we have a debate between Colin and
Lou??)

However, I MUST finish some things NOW, all of which will fully appear on
the fom. Stay tuned.

In this posting, I just want to make some brief comments on two topics
which I hope you will find interesting.

1. About HA/PA. HA is Heyting arithmetic, which is PA with intuitionsitic
logic instead of classical logic. As is well known, there is a simple
syntactic transformation f such that A is provable in PA if and only if
f(A) is provable in HA. What about a syntactic transformation g such that A
is provable in HA if and only if g(A) is provable in PA? It is generally
"understood" that there is no such thing. However, giving an appropriate
theorem to that effect is another matter. First of all, since provability
in both systems is complete r.e., clearly there are low complexity
theoretic translations g. One can even do things like this: HA proves A if
and only if "HA proves A" is provable in PA. But this is obviously
cheating. So what's the theorem? One could define "syntactic
transformation" at first very crudely: simply generalize the look and feel
of the double negation translation. In an appropriate sense, this is
presumably "context free." And then one should be able to prove that there
is no such transformation. But there should be a good very general "no
translation" theorem. Any comments from fom?

2. Develop systematic insight into why a sentence is or is not provable in
HA. Already, this is interesting and not fully treated in the literature
for the easier case of PA. I plan to write what I know about provability in
PA for the fom. But one thing I know nothing about is: when is a pi-0-1
sentence provable in PA? I have no idea, say, why one pi-0-1 sentence is
provable in PA and another is not, of a mathematical nature.

3. In the much harder case of HA, one can start with simple syntactic
classes, and reduce to the case of PA. As Neil has posted, one knows that
HA proves a pi-0-2 sentence if and only if PA proves it. This is due to
Godel in his Dialectica paper. I found an easy syntactic translation - now
known affectionately as "Friedman's translation" - which proves this result
as well as the result for a huge collection of formal systems, including
intuitionistic set theory with some large cardinals, with approximately
.0001% of the effort used for all preceding proofs. (Over 20 years ago).
But then one looks at, say, Boolean combinations of pi-0-2 sentences -
which themselves form an infinite hierarchy - and life starts to get
intriguing. I don't even know when a Boolean combination of pi-0-1
sentences is provable in HA in terms of PA provability.

4. One can also attempt to conduct similar studies for propositional and
predicate calculus.

5. Let me repeat my two favorite items from the set theory/category theory
debate on fom:

From: Charles Silver

>What I'm looking for is a development of category theory, or
>perhaps topos theory, that is based on some underlying *conception*.

>From Feferman 7:15PM 1/16/98:

>... the notion of topos is a relatively sophisticated mathematical
>notion which assumes understanding of the notion of category and that in
>turn assumes understanding of notions of collection and function. ...
>Thus there is both a logical and psychological
>priority for the latter notions to the former.  'Logical' because what a
>topos is requires a definition in order to work with it and prove theorems
>about it, and this definition ultimately returns to the notions of
>collection (class, set, or whatever word you prefer) and function
>(or operation). 'Psychological' because you can't understand what a topos
>is unless you have some understanding of those notions. Just writing down
>the "axioms" for a topos does not provide that understanding. If that is
>granted, and I can't continue further in this discussion if it is not,
>then what work in f.o.m. has to accomplish is a clarification of the
>notions of collection (or class) and function (or operation).

I had the pretentious thought that my various assertions on the fom about
the inadequacy of category theory/topos theory as foundations of
mathematics, and the appropriateness of set theory, would

	a) cause the proponents to have second thoughts and either
elucidate the (nonstandard) notion of f.o.m. that they claim to have, or
	b) cause the proponents to acknowledge that this is o.o.m. and not
f.o.m. (o.o.m. = organization of mathematics).

Reading between the lines, I don't think that Feferman thought that his
extended involvement in this controversy would have effect a) or b), and so
he wrote above, "I can't continue further in this discussion if it is not
[granted]."

I also asserted on the fom that not only do I agree with Feferman, but also
that Silver was never going to find what he is looking for (have you,
Charlie?), and that category theory and topos theory are in no way a
foundation for mathematics any more than graph theory for computer science
or general topology for geometry.

So even if the proponents have not learned anything about this matter from
Sol or me or Silver or Riis or Mayberry or Simpson or a number of others
too numerous to enumerate, I have at least learned something. That I
apparently have not reached that exalted level where I can say "you are
completely wrong" and "you have profoundly misunderstood what f.o.m. is"
and have any effect. There is no question that some people's attraction to
bad ideas is stronger than my powers of persuasion!

This is good to know. Which means that I must do some more important work
in order to reach that exalted level.

6. If I come back to the direct debate, I will discuss my conclusions that
the McLarty axioms are inadequate because of the number of primitives, the
ad hoc hodge podge, the complexity of some of the axioms, the lack of a
single conception, not basing on schemes, no "practical completeness,"
etcetera.

7. So look at the subject line. I have pseudo in parentheses. Which means
that I have a postive proposal for making something out of category
theory/topos theory for f.o.m. By far the most interesting thing about
category theory is the universal mapping properties. Can we define what a
universal mapping property is in general, and determine all of the
universal mapping properties (at least under a very general definition of
universal mapping properties)? If so, then one could hope to reaxiomatize
set theory as the set theory that supports all of the universal mapping
properties.

This would also open the door for making some philosophical sense out of
topos theory as f.o.m.

8. I have tried over the years to come up with something like this in the
traditional setting of sets and set theoretic functions. I do believe that
it can be done, and done with great drama, flair, and power!! I am going to
have a serious new go at this, starting with some confidence. This would be
a new way out of Russell's Paradox, where comprehension is OK when it gives
you something that you can make good mathematical sense out of. In other
words, instead of the inconsistent scheme

the collection {x: A(x)} is a set,

we have the more sophicisticated scheme:

if the collection {x: A(x)} is mathematically useful, then {x: A(x)} is a
set.

9. Then 8 can be translated into category theory; as usual, the category
theorists can follow the lead.