Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
Much-improved version, thanks to deservedly harsh comments from the second anonymous referee, to appear in Logique et Analyse. Preprint at arxiv.org/abs/2103.00090v5.
Slides from a talk on Church’s and my set theories with a universal set, delivered remotely at the University of Oxford Mathematical Institute, October 2013, and at the Stanford Mathematics Department, www-logic.stanford.edu/seminar/1314/…
(See my “A Variant of Church’s Set Theory with a Universal Set in which the Singleton Function is a Set” (abridged), in Logique et Analyse, Vol 59, No 233 (2016), summarized in the “Limitations” slide in www-logic.stanford.edu/seminar/1314/…)
> Where "acc", denoting "is accessible", is defined as what is equinumerous How exactly are you defining “equinumerous”? If by the usual quantification over sets of ordered pairs, you may run into set existence difficulties. This is a severe problem with theories like Church’s Set Theory with a universal set, where it’s not obvious that ill-founded sets have the required mappings. …
A simplified account of the technique is now available in §7.1 of the appendix to my expanded “Naive View of the Russell Paradox,” arxiv.org/abs/2103.00090. (I don’t really expect anyone to read the full exposition in [2016].)
Another indication is that there are still alleged proofs of major theorems where there is genuine disagreement about their correctness. Hilbert’s Program is far from complete.
One indication that this is still a genuine problem with contemporary mathematical practice is how long computer verification of so-called proofs has taken; if they had been genuine proofs rather than proof-sketches, the task would have been straightforward. (This is distinct from discovering proofs, which, as a Platonist, I can allow to be mysterious.) I did once suggest to someone giving a talk on computer proofs at Stanford that he look at Frege, but the two-dimensional formalism would be quite a challenge.
There is of course the sad matter of the inconsistency of his system, but other than that, his rigor still stands as an example to current mathematicians. As a graduate student I found it genuinely difficult, and more of a sociological than mathematical question, to figure out what mathematicians would consider a sufficiently rigorous approximation to a proof. With Frege, that is never in doubt.
