[FOM] New Umbrella?

[Harvey Friedman]

On Sat, Oct 25, 2014 at 6:30 PM, Urs Schreiber
<urs.schreiber at googlemail.com> wrote:
> On 10/25/14, Harvey Friedman <hmflogic at gmail.com> wrote in small part:
>
>> Furthermore, no standard math journal would ever accept a proof
>> written that way.
>>
>> But this is a problem actually being SOLVED - just to what extent, I
>> don't know,
>
> Various people already publish fully formalized mathematics in a
> useful way. It works pretty much like the publication of software, and
> for the same reasons: the formal proof is provided in an appendix or
> in a separate file, and the article itself contains the
> "documentation" that make it enjoyable to read for humans. One recent
> example is [1]. This has become rather standard practice. If you are
> interested, you should maybe talk to these people.

I believe you pointed me to http://arxiv.org/pdf/1302.1207v1.pdf
section  7.3? This is the same kind of unreadable unpublishable
intolerable stuff I am talking about. I can see perhaps that you think
it is better than what Freek wrote. But arguably only somewhat.
>
>> But there are many convenient
>> ways of handling situations like this. It's called extra information.
>> A toy example is f:A into B. Well, the usual way of treating functions
>> is that f:A into B is equaled to f:A into C if the range is contained
>> in B and in C. HOWEVER, as you know, you can talk of functions as
>> pairs (graph(f),B), where you pack the codomain into the function. So
>> you can introduce special variables for "packed functions" F, and use
>> the notation dom(F) and codom(F).
>
> Hm, this misses the point. Are you familiar with the concept of
> isomorphism between mathematical structures?

I enjoyed this insult.

> I'd suggest to go to
> primary sources. In the time it takes to type lengthy mailing list
> messages and wait for replies, an expert on foundations will find
> answers to the questions asked here in the literature. Besides the
> canonical and excellent textbook itself [2], for instance [3] would be
> a good place to read up on the issue of isomorphism invariance.
>
> [1] http://ncatlab.org/nlab/show/p-adic+number#PelayoVoevodskyWarren13
> [2] http://ncatlab.org/nlab/show/Homotopy+Type+Theory+--+Univalent+Foundations+of+Mathematics
> [3] http://ncatlab.org/nlab/show/principle+of+equivalence#CoquandDanielsson

I am going to follow my usual way of proceeding on the FOM when
somebody offers up some "dramatic new and better way of doing things".
I have always requested that the essence of the matter be stated in
very very clear and generally understandable terms that can be readily
debated. discussed, improved on, modified, attacked, and defended,
also in generally understandable terms.

I have always found that unless this is done, the "dramatic new and
better way of doing things" is not what it is advertised to be. That
adherents are not willing to engage in this way, generally for one or
both of these reasons:

1. They themselves do not know how to formulate the essence of the
ideas in a generally understandable way.
2. They know how to formulate it in this way, but choose not to, for a
variety of reasons, including not wanting to enable a large community
of scholars who might make decisive attacks or decisive improvements.
Another name: hiding behind complexity.

Accordingly, as a test case of FOM methodology, I will await generally
understandable explanations of the fundamental ideas behind this
"dramatic new and better way of doing things".

But I do engage in my own kind of homework. I set up private back
channels to see what to expect from people who are at least fairly
knowledgeable - and who, incidentally, HAVE read lots of primary
sources. So I am not quite as much of an ignorant fool as I claim to
be.

OK, let's try to jump start this a bit. You want to complain about how
equality is handled in the Standard Umbrella.

THESIS: Everything general purpose you want to do with equality, the
Standard Umbrella can do better.  Do better for the general math
community, the general philosophy community, and the general logic
community.

The refutation of the above Thesis is not nearly enough to overthrow
the Standard Umbrella, but at least it is a start.

QUESTION: how hard have f.o.m. skilled researchers tried to come up
with a substantial new treatment of equality/isomorphism within the
standard f.o.m. framework? How many man/woman hours in recent years
since f.o.m. became so flexible and highly developed? Is it greater
than zero? And how much time have algebraic/categorical/whatever
people sat down with leading f.o.m. people and asked for an adaptation
of standard f.o.m. for their purposes? Is this greater than zero? I'm
talking about generally understandable inquiries.

Harvey Friedman