The parts I did read seemed to focus on the issue of the actual
existence of mathematical objects. To me, this "actual" existence is
irrelevent. To me, the issue is simply what we talk about when we do
mathematics. If we talk about numbers, and sets and so on, then we
are acting as Platonists. If we talk about formulas (which are about
numbers or sets) then we are acting as formalists. Theorem proving
systems can either manipulate formulas about numbers (anologous to
sentences in conversations between Platonists) or they can manipultate
formulas about formulas which are about numbers (analogous to
sentences in conversations between formalists). Pragmatically, the
Platonic style of reasoning has advantages for both humans and
machines.
Although I believe that Platonism is just a style of reasoning, and
all reasoning is based ultimately on symbol manipulation, I also
believe that the axioms of ZFC have a distinguished status in
mathematics which is not simply a result of arbitrary social
convention. The structure of ZFC is derived from intuitions about
"logical neccessity". Intuitions about the real numbers seem
different, more empirical, than intuitions about domain independent
logic. The axiom of choice is equivalent to the correctness of
Skolemization, a purely logical principle. I believe that our
intuitions about logical neccessity reflect an innate logical system,
a "mentalese". To me, the "clear validity" of Skolemization is
evidence that the axiom of choice is hard-coded into human mentalese.
Replacing choice by AD, and giving up Skolemization, would make my
head hurt (but perhaps other heads have learned to work other ways).
To say that accepting AD would make my head hurt seems different form
saying that AD is false in some deep metaphysical sense. I just think
AD violates the axiom system hard wired into my brain. I choose to
accept the mentalese engine in my brain and "use the force" as it was
so elequently put in a recent message.
David