[FOM] Foundational issues:Friedman/Baez

Wed Apr 6 13:00:21 EDT 2016

That works fine for me.  Bill
> On Apr 5, 2016, at 10:51 PM, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> 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?
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom