[FOM] Formal Proofs

[Urs Schreiber]

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.


> 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'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