[FOM] formal proofs

[David Posner]

Professor Schreiber
Surely, if HoTT mathematics cannot be formalized in set theory then it must be possible to give at least a high level explanation of why that doesn't require diving into a morass of abstractions.  Here's a possible starting point.  My hopelessly naive reasoning on why I believe mathematics can be formalized in set theory goes like this.  Standard mathematical theories are ultimately expressed (or at least expressible) in a standard logic of one kind or another.  The semantics of standard logics are defined in set theoretic terms a la Tarski.  (domains and relations and what not.)  So any standard mathematical theorem can be viewed as a statement about sets and formalized in set theory.  (That may not be the simplest way to
 understand the theorem or formalize the proof but in theory it is possible.)  

So the statement that there are mathematical theorems for which set theoretic formalizations cannot or even might not exist would imply that these theorems and theories (in particular parts of HoTT) are expressed in a non-standard logic or employ a non-standard semantics or both.  Is that in fact the case?  If not, where has my naive reasoning gone wrong?  If so, then can you say something meaningful about where the logic or the semantics deviates from the usual?

On Tuesday, October 21, 2014 3:46 PM, "croux at andrew.cmu.edu" <croux at andrew.cmu.edu> wrote:
 


> Thanks for this informative reply. It looks like however impressive what
we have is, there is still a lot of room for something much better in the
way of absolute rigor.
>
> I haven't really worked on this, but have the ambition to do so in the
following way. Make high level design of a "dream system" from
> scratch, first paying no attention to the present existing
> developments. This will surely lead to a number of interesting and
perhaps clean theoretical questions and theorems. Then present it to
experts in the existing practical systems, who will be able to readily
compare it to reality and criticize.
>

I would be wary of this kind of approach, as it is littered with the
corpses of many ill-conceived proof checkers.
One big issue is that what seems conceptually simple and what is
simple to implement as a proof checker are somewhat different things.

For instance, what foundational system would
 dream of having a complex
module system?
It seems redundant and wasteful. However, any hope of having a practical
system
needs to address this question.


> We can repeat the process using T1 and L1 again. But it would seem that
for this purpose, we may be able to lower the level of T1 and of L1, which
may be a good idea.
>
> Then we continue this process for many steps. Now are we gaining
anything by repetition here? We would if we actually get shorter and
shorter proofs in weaker and weaker L's and weaker and weaker T's. Of
course, at some point, we cannot continue to be reducing. Is there a
natural limit to such a procedure?

A natural limit is PRA, but you can probably get away with less (typically
admitting
only polynomial computable functions). Repetition is not really required:
the main potential for errors is by far in the implementation details, and
this is not
really a
 foundational issue, but more of a problem in computer science and
software
engineering. However, computer scientists have been verifying programs for
decades!

There have actually been a number of contributions in the area of verified
proof-checkers:

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.4582
http://www.cl.cam.ac.uk/~jrh13/papers/holhol.html
http://www.sciencedirect.com/science/article/pii/S157106611200028X
http://www.cs.utexas.edu/users/jared/milawa/Web/
http://dl.acm.org/citation.cfm?id=2103723&dl=ACM&coll=DL&CFID=587690589&CFTOKEN=49655975


> But we need to start somewhere to even define the problem. A purist
starting point would be primitive ZFC, where we have a claim that a given
file constitutes an absolutely correct proof of A in ZFC. Of course, since
we are working with primitive ZFC (no sugar), no human is going to even
look at this monstrosity. There is the problem of even getting a real life
math statement into primitive notation
> absolutely correctly. But I would like to separate off that question,
and take this now for granted.
>

This is the real challenge. The mental abstractions humans use when
stating and proving
theorems are extremely hard to capture, and I think this represents
 the
longstanding
open problem of computer-assisted verification.

More realistically, I think we should investigate manners of capturing
"field-specific" knowledge,
notations and intuition in a way that can be mechanized. It's hard for me
to think of examples,
but "working in the group of endomorphisms" in group theory comes to mind,
as well as "passing to
the dual" in linear algebra or simply just "swapping integrals" in
calculus (or swapping sums, or swapping
differentials and integrals, etc).

Just as there is no "magic bullet" in software engineering, it seems
reasonable that there is no magical
solution to the problem of mechanizing mathematics, but we have already
gone from "unthinkable" to
"possible with a massive amount of time and effort" by incremental
improvements.


> I find this whole approach rather slippery in terms of what the
> details would look like, and
 whether human imperfections are creeping in
in subtle ways. I need to think more deeply about this.

I'm more worried about human leaps of brilliance :)

Best,

Cody





_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20141022/ec573ae3/attachment-0001.html>