[FOM] formal proofs

[Dimitris Tsementzis]

On 16 Oct 2014, at 03:55, Harvey Friedman wrote:
> 
> 2. What is the absolutely simplest watered down specific situation
> that you can explain to anybody where one can get even a glimpse of
> advantages in doing something differently than the usual? I.e., get
> down to the essence of the issues being addressed. 


It is significantly more difficult in FOL/set-theory based proof assistants to prove algebraic theorems that involve keeping track a large number of isomorphisms, as indeed many proofs in modern algebra require. Univalent Foundations (UF) and their implementation in Coq improves on this situation by allowing one to consider ''isomorphism types'' of objects of interest (e.g. groups, topological spaces up to homotopy) as basic entitites. This is as watered-down as I can think, at the cost of becoming slightly imprecise.

> If you can present
> this, then people like me can probably construct many alternatives for
> handling it, some of which may be worthwhile - as well as new
> metatheorems and transfer principles. 

I think what is causing these debates here is a misunderstanding not of the problems that UF solves, but of the problematic it is engaged in. The problematic of UF is not the usual one of set theory, e.g. questions of consistency, equiconsistency, strength of axioms etc. The problematic, rather, is how to remain as faithful as possible to what may be called the "algebraic style" of doing mathematics, while at the same time (i) remaining within a (or possible extensions of a) robust formal/foundational system (e.g. Martin-Lof Type Theory) that also (ii) is naturally implementable in proof-assistants (e.g. Coq). So the kind of problems that UF is trying to solve are not necessarily even of the same type as those that set theory is trying to solve. So to suggest "anything they can do I can do better'' seems like it is missing the point somewhat. UF challenges and improves set theory in at least one respect: the ability to implement "algebraic mathematics" in proof assistants - as indicated above. But set theory was never intended with such a goal in mind and this should therefore not be taken to be a slight. Indeed UF still very much relies on set theory for questions of consistency, reliability etc. (e.g. the first fully worked-out model of UF, the so-called "simplicial model" is constructed in set theory (ZFC+2 inaccessibles) cf. http://arxiv.org/pdf/1211.2851v2.pdf) Voevodsky himself calls ZFC the "benchmark (etalon) of consistency".

> THese are in the arena of
> "special purpose tools" to address the issues. Such work simply cannot
> be done by people who are not trained and steeped in f.o.m. - even if
> they have good credentials.

Work on traditional questions perhaps not. But on questions or remaining faithful to the practice of a certain style of mathematics (e.g. homotopy theory) of course one needs people from outside F.O.M (whatever that means.) If the goal of your system is to faithfulness to practice, then you cannot rely solely on people who are "trained and steeped in f.o.m."

Dimitris


-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20141017/f64cf115/attachment-0001.html>