[FOM] Foundational Challenge

[Joe Shipman]

That means that if you add the scheme “if ZFA proves Phi, then Phi” and call your augmented system ZFA’, then the length of the proofs of the relevant sequence of theorems in ZFA’ scales linearly (really just adding a constant).

In practice mathematicians work in such an augmented system already. They regularly apply metatheorems that certain systems are conservative extensions of other systems, working in the extended systems and concluding that their original system has a proof and therefore that their desired theorem is true.

— JS

Sent from my iPhone

> On Jan 24, 2020, at 8:16 AM, Gabbay, Murdoch <M.Gabbay at hw.ac.uk> wrote:
> 
> 
> > 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.”
> 
> Thanks for asking.  I hope the following response will contain an answer to your specific question.
> 
> Some pointers first: "Equivariant ZFA and the foundations of nominal techniques" is now on the OUP website, here:
> https://doi.org/10.1093/logcom/exz015
> My draft is here:
> https://arxiv.org/pdf/1801.09443.pdf
> 
> To answer your question, Theorem 3.7 of the paper above gives 
> * a schema of ZFA predicates 
> $$
> \phi \leftrightarrow \pi\actingon\phi
> $$ 
> (where $\phi$ ranges over ZFA predicates) and
> * a schema of ZFA derivations of these predicates.  
> 
> $\pi\actingon\phi$ is a predicate in the language of ZFA, obtained by a syntactic manipulation of $\phi$.  $\pi\actingon\phi$ has roughly the same size and shape as $\phi$, though neither is in general a subterm of the other. 
> 
> The proof of Theorem 3.7 is by an induction on $\phi$ (and isn't hard) but note that Theorem 3.7 is a ZFA meta-theorem -- it's a proof about the existence of a ZFA derivations, one for each ZFA predicate.  The length of the concrete ZFA derivation generated for any given instance of $\phi$, scales linearly with the size of $\phi$.
> 
> So from within ZFA, each instance of Theorem 3.7 for a predicate $\phi$, "costs" us $\size(\phi)$ proof-steps --- even though from outside ZFA, the cost is 1 because we have a meta-theorem that tells us it'll work, which we can appeal to by invoking "By Theorem 3.7" (which has constant cost of 14 characters).
> 
> I quote a quadratic blowup because in practice, for the kind of mathematics which EZFAC was designed to support, we typically want Theorem 3.7 for every $\phi$ in our development.  
> 
> If we consider a paper, or a development in a theorem-prover, consisting of a sequence of predicates $\phi$ of linearly increasing length $1, \dots, n$, then the cost of applying Theorem 3.7 repeatedly scales quadratically in the number of predicates overall (not including those predicates involved in proving instances of Theorem 3.7 itself).
> 
> Two clarifications:
> I quote ZFA above, not ZF, but this is purely for convenience.  The same issues arise in ZF, and indeed we tend to be worse off in ZF in the sense that it can be somewhat harder to see and state the relevant results.  
> I discuss this elsewhere in the paper and don't want to get hung up here on the difference in this post.
> To the reader who may be put off by the artificiality of my example above (predicates of linearly increasing length ...) I note that the "quadratic blowup" problem is a real thing which is observed in practice and can be surprisingly robust and persistent across variations in solutions to the problems which nominal techniques try to address.  
> To be clear, I do not claim that nominal techniques are the only solution to the problem which I designed EZFAC to solve, rather, I note that ZF-based approaches can exhibit persistent proof-blowups (and related difficulties, as discussed in my recent paper and others) when applied to a certain basket of issues in computer science, and at the very least, the EZFAC paper proposes an analysis of the deeper issue using the language of FOM -- and in particular using "alternative foundations" -- as well as a suggestion on how to solve it.
> 
> Jamie Gabbay
> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200124/f893fe2d/attachment-0001.html>