869: Structural Proof Theory/1
Harvey Friedman
hmflogic at gmail.com
Wed Feb 24 00:10:44 EST 2021
No, I am not founding yet another new field called "Structural Proof Theory".
DIGRESSION: I am very busy polishing up material in my 54 year project
(Tangible Incompleteness) which involves very major developments in
Tangible Incompleteness which I really want to tell you about when my
proofs are finished. It's taken some time but close to finishing the
Order Invariant Maximality part. In two dimensions totally suitable
for gifted high school programs, and for dimension three (to be
verified) already way beyond ZFC. More soon... Also because of that I
haven't got into the next major problems in SMAT = Structural Mapping
Theory, and want to get some more results for the next postings on
that.
So back to this posting on Structural Proof Theory.
WARNING: I remain rather distant from the Proof Assistant field, and
my main contact used to be Jeremy Avigad some years back. Also I had
some brief interesting encounters with John Harrison. I remember with
great interest his "Make Set Theory Great Again". I was pushing a
heavily set theoretic anti type theory approach at a meeting in
Toronto and he was very positive about it (I don't take credit for his
enthusiasm, of course). Most of the illustrious participants at that
meeting were horrified and amused by me but when Harrison indicated
approval I sensed some shock.
SOME HARRISON TALKS
http://aitp-conference.org/2018/slides/JH.pdf
https://www.cl.cam.ac.uk/~jrh13/slides/wollic-23jul15/slides.pdf
https://www.cl.cam.ac.uk/~jrh13/slides/fmsummerschool-18may15/slides.pdf
https://www.cl.cam.ac.uk/~jrh13/slides/ihp-05may14/slides.pdf
https://www.cl.cam.ac.uk/~jrh13/slides/lyon-03feb14/slides.pdf
https://www.cl.cam.ac.uk/~jrh13/slides/lms-29oct13/slides.pdf
SOME HARRISON PAPERS
https://www.cl.cam.ac.uk/~jrh13/papers/joerg.html
https://www.cl.cam.ac.uk/~jrh13/papers/mark10.html
https://www.cl.cam.ac.uk/~jrh13/papers/notices.html
https://www.cl.cam.ac.uk/~jrh13/papers/ab.html
SPT definitely exists in multiple guises but I don't think it goes
very far in the directions I have been looking for for a long time. It
really has been my vision for what I would HAVE LIKED to see come out
of the field Proof Assistants. .
Actually, being rather distant from the Proof Assistant field,
dabbling around the edges, occasionally thinking I have a better way
of doing things, never following through much, I am of course quite
ignorant about the details of what is going on there and am very happy
to see Chow's very recent posting on this.
https://cs.nyu.edu/pipermail/fom/2021-February/022494.html
1. WHAT KIND OF MATHEMATICAL ACTIVITIES CAN REALISTICALLY BE AFFECTED
BY PROOF ASSISTANTS?
There is a lot of material on this in those Harrison talks/papers I
compiled above. But here is my naive take on this.
Once upon a time there was the idea that although there was a clear
sense of rigor in mathematics, that it was an objective matter, that
there is so much complications going on and so much "mathematical
intuition" and "mathematical feel" to actually get anything done, that
any kind of ultimate form of rigor was hopelessly fictional. And also
if even achievable, would result in monstrous works not only totally
incomprehensible, but also of completely absurd length. That it may
not even be possible to give any perfectly rigorous proof of a
complicated theorem especially like FLT or Finite Simple Groups
theorem, or even much less complicated proofs, in any kind of feasible
space. That unravelling ultimate rigor has an inherently exponential
component to it, that in the unravelling into perfect rigor, there
will be constant factor multiples that get iterated, and result in
things that cannot actually exist in the known physical universe.
I CONSIDER IT A MAJOR FOUNDATIONAL EVENT THAT THIS HAS BEEN DECISIVELY
REFUTED OR ALMOST DECISIVELY REFUTED. THIS WAS ROUTINELY USED AS AN
ATTACK AGAINST FOUNDATIONS OF MATHEMATICS GENERALLY BY MATHEMATICAL
LEADERSHIP.
It is still true that normally speaking, we get monstrous unreadable
monstrosities. But this also has been addressed at least somewhat.
Although I don't know of a fully readable ultimately rigorous text
book where the book just looks a little stiff - sort of like some of
the uninspiring professors we know of (maybe ourselves). But totally
readable. LIke to see that done.
Now there has always been a much more ambitious aim. Ultimately to
make Proof Assistants a serious tool for ORDINARY PROFESSIONAL
MATHEMATICAL ACTIVITIES especially activities surrounding
a. Getting a Theorem proved in the sense of before any manuscript,
where the "proof" lies in mental images and scribbles on a piece of
paper or computer screen. Before any serious checking.
b. In the serious checking stage before writeup.
c. In the writeup stage constructing a first manuscript meant to
"verify" that it's all there for me only. Generally no one else would
get much out of it.
d. Perfecting the writeup so that it can be used to give a detailed
seminar presentation somewhat understandable to some experts other
than the author..
e. Perfecting the writeup further turning it into a real preprint
publicly available so advanced students can really get a good sense of
what is going on.
These are all separate stages for a significant new theorem. Nowadays
I do this all for free, more of it than ever before. And I can
honestly tell you that the last thing I look for to help with this is
a Proof Assistant. I really get more help from a good meal. The
thoroughly rewarding absolutely horrific pain and contortions and
frustrations involved in these activities are rather difficult to
describe to the non mathematician. I get immersed in a sea of flimsy
fragile understanding, at least until somewhere in d.
HOWEVER, although any usual kind of ultimate rigor here plays no role,
there is a CERTAIN LEVEL OF RIGOR in a sweet spot between what is
going on in a,b, and what is going on in c. In c it is demanded that
the definitions and lemmas and theorems are laid out "correctly" with
all defaults laid out (things must be nonzero, the case k = 0 makes no
sense and needs k >= 1, no inappropriate reuse of symbols, no
ambiguities, and so forth). BUT AGAIN, don't see any use for proof
assistants in the normal course of events here.
Then there is this:
f. Having a Proof Assistant check for correctness.
Obviously this cannot be done with the normal form that e) takes. BUT
AT THIS POINT IN TIME, doing this is extremely time consuming and the
question remains: WHAT REWARDS DO WE GET OUT OF DOING THAT?
The rewards seem to me to start to appear mainly in two VERY SPECIAL situations.
a. MATHEMATICAL ICONS that have long been accepted by the math
community as having been done by normal professional standards. There
is no normal doubt of any kind but the stuff is so fundamental and
well understood that it would be "nice" to have it formally verified.
Although I do value this work, it does seem that, especially for the
normal garden variety important mathematical result of which there are
dozens proved every year worldwide, that this REQUIRES MUCH MORE
JUSTIFICATION for the investment.
b. SITUATIONS where there really is a question of correctness. A
history of errors maybe in and around the development.
OVERALL OPINION. The prospects for Proof Assistants being seriously
useful for everyday garden variety serious mathematical developments
look extremely remote for the foreseeable future. However, we all know
something about some VERY SPECIAL SITUATIONS where there is a point in
using them. In general, I like the investment in many of these. But
THEY ARE UNUSUAL.
It would be interesting to REALISTICALLY formulate what kinds of
situations and activities.
What I consider really neglected, as far as I can tell, are some other
aims both practical and THEORETICAL.
2. SOME NEW PRACTICAL AIMS FOR PROOF ASSISTANTS - later
3. WHAT IS ULTIMATE RIGOR ACTUALLY? FOUNDATIONS OF CERTAINTY - later
4. WHAT CAN AND SHOULD AND WILL STRUCTURAL PROOF THEORY LOOK LIKE? - later
##########################################
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 868th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-799 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/
800: Beyond Perfectly Natural/6 4/3/18 8:37PM
801: Big Foundational Issues/1 4/4/18 12:15AM
802: Systematic f.o.m./1 4/4/18 1:06AM
803: Perfectly Natural/7 4/11/18 1:02AM
804: Beyond Perfectly Natural/8 4/12/18 11:23PM
805: Beyond Perfectly Natural/9 4/20/18 10:47PM
806: Beyond Perfectly Natural/10 4/22/18 9:06PM
807: Beyond Perfectly Natural/11 4/29/18 9:19PM
808: Big Foundational Issues/2 5/1/18 12:24AM
809: Goedel's Second Reworked/1 5/20/18 3:47PM
810: Goedel's Second Reworked/2 5/23/18 10:59AM
811: Big Foundational Issues/3 5/23/18 10:06PM
812: Goedel's Second Reworked/3 5/24/18 9:57AM
813: Beyond Perfectly Natural/12 05/29/18 6:22AM
814: Beyond Perfectly Natural/13 6/3/18 2:05PM
815: Beyond Perfectly Natural/14 6/5/18 9:41PM
816: Beyond Perfectly Natural/15 6/8/18 1:20AM
817: Beyond Perfectly Natural/16 Jun 13 01:08:40
818: Beyond Perfectly Natural/17 6/13/18 4:16PM
819: Sugared ZFC Formalization/1 6/13/18 6:42PM
820: Sugared ZFC Formalization/2 6/14/18 6:45PM
821: Beyond Perfectly Natural/18 6/17/18 1:11AM
822: Tangible Incompleteness/1 7/14/18 10:56PM
823: Tangible Incompleteness/2 7/17/18 10:54PM
824: Tangible Incompleteness/3 7/18/18 11:13PM
825: Tangible Incompleteness/4 7/20/18 12:37AM
826: Tangible Incompleteness/5 7/26/18 11:37PM
827: Tangible Incompleteness Restarted/1 9/23/19 11:19PM
828: Tangible Incompleteness Restarted/2 9/23/19 11:19PM
829: Tangible Incompleteness Restarted/3 9/23/19 11:20PM
830: Tangible Incompleteness Restarted/4 9/26/19 1:17 PM
831: Tangible Incompleteness Restarted/5 9/29/19 2:54AM
832: Tangible Incompleteness Restarted/6 10/2/19 1:15PM
833: Tangible Incompleteness Restarted/7 10/5/19 2:34PM
834: Tangible Incompleteness Restarted/8 10/10/19 5:02PM
835: Tangible Incompleteness Restarted/9 10/13/19 4:50AM
836: Tangible Incompleteness Restarted/10 10/14/19 12:34PM
837: Tangible Incompleteness Restarted/11 10/18/20 02:58AM
838: New Tangible Incompleteness/1 1/11/20 1:04PM
839: New Tangible Incompleteness/2 1/13/20 1:10 PM
840: New Tangible Incompleteness/3 1/14/20 4:50PM
841: New Tangible Incompleteness/4 1/15/20 1:58PM
842: Gromov's "most powerful language" and set theory 2/8/20 2:53AM
843: Brand New Tangible Incompleteness/1 3/22/20 10:50PM
844: Brand New Tangible Incompleteness/2 3/24/20 12:37AM
845: Brand New Tangible Incompleteness/3 3/28/20 7:25AM
846: Brand New Tangible Incompleteness/4 4/1/20 12:32 AM
847: Brand New Tangible Incompleteness/5 4/9/20 1 34AM
848. Set Equation Theory/1 4/15 11:45PM
849. Set Equation Theory/2 4/16/20 4:50PM
850: Set Equation Theory/3 4/26/20 12:06AM
851: Product Inequality Theory/1 4/29/20 12:08AM
852: Order Theoretic Maximality/1 4/30/20 7:17PM
853: Embedded Maximality (revisited)/1 5/3/20 10:19PM
854: Lower R Invariant Maximal Sets/1: 5/14/20 11:32PM
855: Lower Equivalent and Stable Maximal Sets/1 5/17/20 4:25PM
856: Finite Increasing reducers/1 6/18/20 4 17PM :
857: Finite Increasing reducers/2 6/16/20 6:30PM
858: Mathematical Representations of Ordinals/1 6/18/20 3:30AM
859. Incompleteness by Effectivization/1 6/19/20 1132PM :
860: Unary Regressive Growth/1 8/120 9:50PM
861: Simplified Axioms for Class Theory 9/16/20 9:17PM
862: Symmetric Semigroups 2/2/21 9:11 PM
863: Structural Mapping Theory/1 2/4/21 11:36PM
864: Structural Mapping Theory/2 2/7/21 1:07AM
865: Structural Mapping Theory/3 2/10/21 11:57PM
866: Structural Mapping Theory/4 2/13/21 12:47AM
867: Structural Mapping Theory/5 2/14/21 11:27PM
868: Structural Mapping Theory/6 2/15/21 9:45PM
Harvey Friedman
More information about the FOM
mailing list