[FOM] Alternative Foundations/philosophical

[Harvey Friedman]

>
> Dear Harvey,
> How many layers of coding will you accept for a problem and still
> consider it as being "in the usual set-theoretic foundations"? In
> practice, most people work in a foundation-agnostic way, especially if
> they work in so-called 'ordinary mathematics' (for which not the full
> strength of ZFC is needed). For sure, one could code work on schematic
> homotopy types into ZFC (possibly with an inaccessible, but I strongly
> suspect it's not necessary), but actually writing them down in
> set-theoretical language *in detail* would be masochistic (reminiscent
> of Bourbaki's empty set
> http://www.neverendingbooks.org/content/empty-set-according-bourbaki).
> >
> *From the point of view of category theory, almost all of it seems *rather
> natural and in fact in some ways universal (in the category
> theoretic sense: being the optimal/smallest way of getting such a
> thing). From the point of view of homotopy type theory, this should be
> just a non-standard model of the axioms (this isn't proven, but from
> what I understand, it's expected).
> This is not a 'simple example', because I'm not playing the 'my
> foundation is more convenient than yours' game. At some point work on
> problems become so far removed from foundations that the choice of
> foundations becomes moot. Do we prefer foundations that are closer to
> mathematical practice, or foundations with an economy of symbols and
> concepts when written in first-order logic? Pick whichever makes you
> sleep at night assured that your work is no more contradictory than
> the foundations.
> Chasing down an example understandable by an mathematics graduate
> which, when written in one foundation is longer than when written in
> another foundation is like comparing axiom systems purely on the
> number of characters they require when printed on the page. Vaguer
> criteria such as "comparatively awkward" are unbecoming of logicians.
> Best regards,
> David


I have been concerned with philosophically coherent foundations. I.e.,
ultimate foundations, particularly ultimate general purpose foundations.
Obviously I have no problem with referring to a philosophically coherent
general purpose foundation, set up with philosophical clarity, and then
immediately making all sorts of special purpose constructions within that
philosophically coherent general purpose foundation that serves all kinds
of important mathematical purposes. It is not true that any interesting
mathematical system that is interpretable in a philosophically coherent
general purpose foundation is itself philosophically coherent as a
foundation. Issues like this seem to surface especially when one is engaged
in nonstandard manipulations of the primitives - particularly equality.
This is an issue at several levels, including proof assistants. See, e.g.,
http://www.cs.nyu.edu/pipermail/fom/2014-February/017850.html (especially
the last paragraph),   and also the related
http://www.cs.nyu.edu/pipermail/fom/2014-February/017859.html
http://www.cs.nyu.edu/pipermail/fom/2014-February/017854.html
http://www.cs.nyu.edu/pipermail/fom/2014-March/017877.html

In particular, I am interested in whether the following is true:

Anything of general intellectually interest ing foundational aim that you
can achieve with alternative foundations you can achieve better (more
clearly, more generally understandable, more coherently, more powerfully,
etc.) with the usual foundations.

So far, I haven't seen any candidate counterexamples of this kind spelled
out on the FOM in order to see if the above is the case. If someone
proposes a counterexample, the fact that I don't or can't respond with a
counter argument is of course not even remotely decisive. I have my own
limitations as does everybody else that I know. Not only that, I could be
wrong.

Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140307/204a6a87/attachment.html>