[FOM] Foundational issues:Friedman/Baez

[Harvey Friedman]

More Friedman/Baez.

Friedman:

"In other words, you only recognize finished calculated demonstrations
of Sigma-0-1 sentences  as matter of fact."

Baez:

"I didn't say anything about "Sigma-0-1 sentences".  I said:"

"To me the only "matter of fact" in mathematics is that a given set of
rules for manipulating expressions can be used to derive a given
expression."

The expressions can be of any sort whatsoever, as can the rules.  And
the "matter of fact" is not what the final expression "says" (since
this is largely in the mind of the person reading it), but rather,
that the expression has been derived using the given rules (which is
something we can usually agree on). "

What you are describing is exactly the explicitly witnessing of
Sigma-0-1 sentences in the usual standard f.o.m. sense. Sorry if that
was confusing.

We use the hierarchy

Pi-0-1, Sigma-0-1, Pi-0-2, Sigma-0-2,...

for the usual arithmetic hierarchy of sentences. For Gershom B - this
is not just of matter of cardinality, but of quantifier alternation. I
will respond separately to Gershom B in greater detail.

Here I assume that you are talking about strictly finitary rules, with
derivations immediately subject to computer check? What if the sizes
are far beyond computers?? We actually have theorems to the effect
that there are situations like that where something bit sized is
derivable from bit sized rules, but the derivation is incredibly long,
and cannot be proved to exist by computer. In fact, the only proofs of
the mere existence of the finite derivations use massively infinite
reasoning - or if they don't use massively infinite reasoning, then
they must be far too long - at least 2^2^2^2^2^2^2^2^2^2^2^2 bytes.

"Perhaps "can be used" is a bit too subjunctive.  What I mean is that
if I tell you a list of rules for manipulating expressions, and clam
that a sequence of expressions is obtained by repeatedly following
these rules, you can - with enough patience, and maybe a computer -
check to see if it really does."

As I said above, what methods do you allow for proving that "even a
single bite sized expression is obtained by repeatedly following your
even bite sized rules?" There are even mathematically interesting
examples of this, not just ad hoc.

Friedman:

"Maybe you are in fact an ultrafinitist, this I don't know."

Baez:

"I don't think so.  The ultrafinitists I know seem to have positions
on whether certain mathematical entities "really exist", which seem to
make them reluctant to, say, use certain methods of proof.  I'm happy
to use pretty much any method of proof, as long as the method and
result seem interesting to me."

I can't really tell from that. A typical ultrafinistist like the late
Yesenin Volpin, would say of 2^1000, that he has no good idea of what
this refers to, but would not outright say that it doesn't really
exist. He would say, "if you think that that expression refers to
something, show me what you are talking about". The late Ed Nelson
also had similar views, although he gladly participated in a lot of
stuff that does not meet such strict criteria.

Your last sentence above seems to me to give you the freedom of
packing a lot of foundational issues and difficulties with
finitist/formalist positions into the word "seems interesting to me".
Perhaps so much so that in order to really engage the issues, we might
have to take up the matter of the foundations of "interesting to
Baez".

Friedman:

"Of course you can say, "pick those axioms/rules that are useful". But
I am skeptical that one can use "useful" as a principled driver for
the choice of axioms/rules, while avoiding matter of factness."

Baez:

"I think I emphasized that good rules are interesting, rather than
that they're useful.  But they're both relevant criteria: the former
more in pure mathematics, the latter more in applied mathematics."

In my response, I moved to a difficulty for the finitist/formalist
positions, which is the choice of "good rules". One very important
criteria that (almost everybody thinks) has to be met is consistency
(this usually can be formulated without using jargon from math logic).
But how do you tell whether a given set of even very interesting and
be sized rules are in fact consistent? That's a Pi-0-1 sentence, not
capable of Baez-witnessing like Sigma-0-1 sentences.

"I don't expect these criteria to ever definitively settle the
question of "which rules we should use", any more than Darwinian
evolution ever definitively settles the question "what an organism
should be like".  Instead, the passage of time winnows out some
things, while others thrive - both living creatures and systems of
mathematics.  This process is incredibly complicated and not easily
summarized."

Makes sense to me. But there are some great scientific handles here,
and in terms of general purpose, they have all come out of totally
philosophically coherent (at least now totally subsumed in) standard
f.o.m.  development. The biggest handles here have been around for
thousands, and hundreds of years just like two hands, two feet, one
head, etc. E.g.,

propositional logic
equational logic
predicate logic
arithmetic induction/recursion
geometric continuum
set comprehension
finitary rules/derivations/formal systems
interpretations
consistency and relative consistency
completnenss
incompleteness
complexity of statements
models of sentences
...

As I will reply to Gershom B, interpretations are extremely powerful
and subtle, and rule us all.

"I also don't consider it my role to decide what formalisms other
mathematicians should use, or adjudicate among them.  I like some
better than others, and if people want my advice I'm happy to give it,
but I don't believe in trying to "lay down the law".  "

Wouldn't you want to be one of the founders of the US Constitution,
involved with Federalist Papers and the like, trying to "lay down the
law" in some incredibly deep principled way? You seem smart enough to
have been a good participant in that.

Friedman:

"OK, so can you give me some interesting first principle ideas about
"reversible path or process leading from x to y" that has some
intellectual traction?"

Baez:

"I've already said I don't have the energy to explain the
"homotopification" or "n-categorification" program in a way that will
satisfy you.   I have papers about that, and there's the HoTT book...
but you probably won't like them.  I only brought up the issue again
to emphasize that when you talk about "the really crucial issues in
the foundations of mathematics", those aren't the issues that I
consider crucial.   I'm not trying to convince you that my way of
thinking has merit; I just wanted to point out the gulf dividing us. "

I'm quite content with this, as long as you agree with something you
may not agree with: that there is something seriously missing here,
that is an integral part of why certain mathematical developments rise
to the top iconic level that stands the test of history, and has great
general intellectual significance.

On the other hand, I would be rather disappointed if this is mainly a
comment about how silly I am being in requiring such "philosophical
coherence" and using such a strong sieve.

Look, I have the energy to recast the great standard f.o.m. with all
of its spectacular open issues, to outsiders. It's been done at about
half the quality level really needed to make the crucial points -
crucial points that are simply not understood by outsiders, at least
not properly.

So where is my book on standard f.o.m.? Well, I have been busy dealing
head on with the biggest issues, for 50 years or so, and I also simply
did not come across anyone who even asked me to explain real standard
f.o.m.

Interesting asymmetry here. I ask for philosophically coherent
explanations of alternative foundations, and I get either blank stares
about what the hell "philosophical coherence" means, or I get - quite
reasonably - people saying that they can do this but it is too time
consuming.

So from my perspective, until I see a clear market for it, and I have
never seen such a market for it, I won't be doing what I am asking you
to do on your side, except episodically through these internet
outlets. Instead, I will continue to try to deal with the biggest
issues on my side.

Let me try something once more. Are these crucial issues? I could list
more, but these two should be useful to discuss.

1. How, why, or should we believe that the various axioms/rules that
have substantial adherents, not only in standard f.o.m., are
appropriate, and in particular are free of contradiction? (Because of
interpretations, this issue has a crucial core that is independent of
choice of foundations).

2. Do the various axioms/rules that we use allow us to successfully
develop areas of CONCRETE mathematics that we find perfectly naturally
interesting, or do we need to expand these setups? For the purposes of
concrete mathematics, we have been adhering basically to a setup that
got engraved in stone around 1920. That is a very very long time for
something like this.

As you well know, Kurt Goedel made monumental discoveries concerning
1,2, but very very far from being conclusive.

I have a feeling that you do not regard these as crucial issues. But
note that 1,2 above have a great deal of specificity and history and
prima facie philosophical coherence.

So could you list two crucial issues from your point of view, with
similar specificity and prima facie philosophical coherence?