[FOM] Foundational Challenge

[Gabbay, Murdoch]

> 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 [and] In practice mathematicians ... 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.

Yes, I agree.  And indeed EZFAC is just an extension of ZFAC with an axiom-scheme of theorems that are (by Theorem 3.7) derivable in ZFA.

If the reader is comfortable with first-order theories, with how to move between them, and with the difference between a theorem and a meta-theorem, then the moves between ZFC and EZFAC are easy.

However, I need to put this agreement in a broader context please:


  *   In a theorem-prover, meta-theorems are not as generally available -- "no handwaving".
There are things like Isabelle "tactics" -- which for the purposes of this message can be viewed as programmed meta-theorems -- however, the tactic relevant to proving Theorem 3.7 turns out to be hard to automate in full generality.  (I imagine that the schema “if ZFA proves Phi, then Phi” would be similarly hard.)
This tends to make the choice of foundation more acutely felt.

  *   Readers, even experienced ones, tend to treat meta-theorems of fields that they are unfamiliar with, with suspicion.
So specifically, even if a meta-theorem is true of ZF(A), the burden of explaining to a randomly-chosen reader/referee what a FOM meta-theorem even is (if required), and then convincing them that this particular meta-theorem should be believed, sucks air away from the interesting maths.
I've spent too much of my career trying to make meta-theorems look easy, and they're just not: a good meta-theorem tends to express a deep understanding of the global structure of a theory, and this is not necessarily something a reader can pick up in a hurry, unless they are very practised.

  *   In practice, the equivariance result Theorem 3.7 of EZFAC can be hard to see and state, when phrased in ZF.  It's obvious because the EZFAC foundation itself is designed make it look easy.
In my paper I talk about properties that are "natural ZFA theorems", meaning --- not that they can't be phrased in ZF but --- that this is where they are easily and naturally stated.

In short, from my experience the threshold is too great: I'm not a good enough expositor to take a reader steeped in ZF to an understanding of the things EZFAC was designed to do, from a cold start --- and it can be hard to manipulate things that are (arguably) natural EZFAC properties, in a system (formal or informal) that is premised on ZF.

Thus essentially the argument of my paper is that for certain purposes we might be better off just asserting EZFAC -- *even though* we know it's in meta-mathematical principle epsilon away from ZF -- and building the development from there.

I realise this was a very long answer to your short comment, but I have written it in this detail to make clear to a reader why I responded to the original challenge, which was to give an example of an "alternative foundation" such that

 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

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:

  1.  Heriot-Watt University, a Scottish charity registered under number SC000278
  2.  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/2c9236cc/attachment-0001.html>