[FOM] Foundational Challenge

[Joe Shipman]

Can you please state a precisely worded proposition explaining what you mean by “quadratic blowups”?

My impression is that you mean “in my alternative foundational scheme, there is a class of theorems whose proofs, when translated into ZFC in the standard way, increase in length by a quadratic function.”

However, if you can prove that, then either your foundation proves things about sets that ZFC doesn’t (if it is stronger than ZFC), or there is no genuine quadratic blowup (If it is sufficiently weaker than ZFC that ZFC proves its soundness), or something strange in between. 

— JS

Sent from my iPhone

> On Jan 14, 2020, at 2:59 PM, Gabbay, Murdoch <M.Gabbay at hw.ac.uk> wrote:
> 
>  ​> I CHALLENGE YOU TO IDENTIFY:
> 
> > An EXAMPLE of mathematics done in any “alternative foundation” to set theory, where EITHER
> > a) it is not obvious that any result derived that is statable in set theory will be provable in ZFC plus a large cardinal of some kind
> > OR
> > b) it is an ARITHMETICAL result with a significantly shorter formal derivation from first principles than is possible in ZFC (“significantly” means “more than the usual amount of work to translate proofs formalized in Second Order Arithmetic into ZFC proofs”, which is a well-understood quantity).
> 
> I've been working on a concrete instance of this.  In 
>    "Equivariant ZFA and the foundations of nominal techniques" 
> (to appear in the Journal of Logic and Computation; available online at https://arxiv.org/abs/1801.09443)
> I describe an alternative sets foundation EZFAC on ground similar to item (b) above.
> 
> EZFAC is very close to ZFC and easily proved equivalent to it.  
> 
> But, there's a class of proofs called "renaming lemmas" or "equivariance lemmas" which in ZFC tend to expand quadratically in the size of the overall development.  Renaming lemmas turn up in certain specification and verification proofs, and the quadratic blowup is a well-known phenomenon in certain circles, which can prove a significant difficulty in practice (especially, but not exclusively, in theorem-provers).  
> 
> I argue that in EZFAC, the cost of equivariance lemmas reduces to near-constant time, and that these lemmas are easier to see, state, and prove.  Much of the effort devoted in practice to automating or avoiding renaming/equivariance lemmas, can be traced to the use of a foundation imperfectly suited to the proofs required by the mathematics, and (so I argue) we should consider using EZFAC instead.  
> 
> I suspect that the cost of implementing EZFAC (or even a type theory based on it) would be relatively slight.
> 
> Slight change of focus now: I would also argue that as well as
>    "alternative foundations" 
> we should be discussing
>    "domain-specific foundations", 
> this being a deliberate riff on "domain-specific languages" --- as it becomes more routine to automate proofs (due to size, security, or social norms), some parts of mathematics will come to resemble software development.  The converse process, that some parts of software development are coming to resemble mathematics, and specifically formal logic, is already well under way.  
> 
> Therefore, we can expect to see more debates about the pros and cons of foundations, many of which will be couched in terms of what an engineer can reliably produce in a given time using available tools.  Some of the participants in these discussions may not even realise they're discussing what the FOM community would call foundations!
> 
> Jamie Gabbay
> 
> Heriot-Watt University is The Times & The Sunday Times International University of the Year 2018
> Founded in 1821, Heriot-Watt is a leader in ideas and solutions. With campuses and students across the entire globe we span the world, delivering innovation and educational excellence in business, engineering, design and the physical, social and life sciences. This email is generated from the Heriot-Watt University Group, which includes:
> Heriot-Watt University, a Scottish charity registered under number SC000278
> Heriot- Watt Services Limited (Oriam), Scotland's national performance centre for sport. Heriot-Watt Services Limited is a private limited company registered is Scotland with registered number SC271030 and registered office at Research & Enterprise Services Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS.
> The contents (including any attachments) are confidential. If you are not the intended recipient of this e-mail, any disclosure, copying, distribution or use of its contents is strictly prohibited, and you should please notify the sender immediately and then delete it (including any attachments) from your system.
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200117/ecc9b192/attachment.html>