871: Structural Proof Theory/3
Harvey Friedman
hmflogic at gmail.com
Sun Feb 28 21:27:32 EST 2021
There is a line of investigation that I should have stated clearly
earlier that I think should be able to be mined with rather
interesting consequences
We typically have a system like PA and ZFC and a sentence A in its
language which has been proved in PA or in ZFC. THis means that we
have found a FINITE fragment T of PA or ZFC which LOGICALLY IMPLIES A.
We call these the SUFFICIENT fragments.
The most obvious issue that arises already is this. What can we say
for the various theorems of mathematics in PA or in ZFC, about these
SUFFICIENT FRAGMENTS? Let us distinguish the following for a
mathematical theorem phi.
1. The actual sufficient fragment used in a proof of phi in PA or ZFC.
If the proof has been done in a proof assistant, then naturally we
have good access to what sufficient fragment was used in that proof.
2. Possible sufficient fragments that could be used in a proof of phi
in PA or ZFC.
QUESTION A. For the entire corpus of mathematical theorems proved in
proof assistants, compile a list sufficient for all of them. What is
its size? What is the maximum number of quantifiers used in any one of
them And so forth.
Now there is something NAIVE about the CRUDE way I have formulated
this Question. It doesn't take into account the extended use of
abbreviation power usedin proof assisted proofs - or human ones also.
So the Question needs to be modified.
Each mathematical theorem of PA/ZFC is proved using PA/ZFC by a series
of definitions, each building on top of previous ones, and the quoting
of instances of PA/ZFC using these definitions. I will call that THE
QUOTE STRUCTURE of the proof. It isn't at first glance apparent that
this is robust enough, but it does seem to be reasonably so.
Fortunately it is thanks to the structure of the axioms schemes in
PA/ZFC. They say for all formulas such and such simple modification of
it is an axiom. And things are solid enough that we can obviously
simply extend that to all formulas in the extended languages involved
that come from the hierarchy of definitions. They can all be counted
too as formulas without qualification.
So QUESTION A is entirely appropriate upon reflection, allowing for
the hierarchy of definitions in the proofs.
But now we need to BACK UP. We have been compelled to come to Question
A, and then realize how important definitional structure is. SO LET US
TALK ABOUT DEFINITIONAL STRUCTURE independently of proofs!!
QUESTION B. What can we say about the DEFINITIONAL STRUCTURE of
mathematics based on PA/ZFC? Note that each concept introduced by a
definition points to a list of other concepts previously introduced
and these point to yet other ones, until we get back to the primitives
of PA/ZFC. WE HAVE DEFINITIONAL TREES. What do these DEFINITIONAL
TREES LOOK LIKE? In terms of size and depth, say. Also the trees are
labeled and so what can we say about the repeated labels? And are the
trees of a different shape according to the area of mathematics that
they arise in? E.g., how does number theory and algebraic geometry and
operator theory and differential geometry compare in depth (lol)?
There is a second category of trees here. There are the rather sizable
trees coming from unravelling the advanced concepts back to the
primitives. But there are also the little tiny by comparison trees
arising from each individual definition. What can be say about those
tiny trees - LOCAL DEFINITIONAL TREES? It would seem that some of
these occur over and over again.
Now I have a fundamental question concerning the choice of SUFFICIENT FRAGMENTS
QUESTION C. Relative to the Sufficient Fragments chosen, the proof is
conducted with PURE LOGIC. How much of the work involves quoting the
sufficient fragment, and how much of the work involves only pure
logic? Do we really have a situation where maybe the purely logical
part is comparatively TRIVIAL and all of the hard work is the quoting
part? The quoting part generally speaking should include the
definitional part. So in such a model of what is going on in math and
in proof assisted math, all of the hard work would be in choosing the
right definitions and quoting the right axioms, or even automatically
quoting the axioms involving the right definitions (don't know whether
I should have said that), AND THE ACTUAL THING CALLED *REASONING* is
either trivial or comparatively trivial, AND MAYBE FULLY AUTOMATIC
even with the present primitive proof assistant tools???
ALERT: In looking over this posting, I now realize that there is a
component in the PURE LOGIC side which I think does blow up from time
to time. And that is APPLICATION OF PREVIOUSLY ESTABLISHED LEMMAS AND
THEOREMS. There we may well apply them to COMPLEX TERMS that are not
simply lying around.
I.e., can we ENVISION the following?
QUESTION D. Can a satisfactory fully rigorous treatment of mathematics
be given along the following lines. A whole series of judicious
DEFINITIONS, with statements of Lemmas and theorems, and NO PROOFS
WHATSOEVER except building up sufficient fragments along the way, and
also writing down APPLICATION TERMS, i.e., terms to which previous
statements are to be applied.In other words, you have a theorem, built
on previous theorems and lemmas, and you simply quote all of the axiom
instances that are relevant, and you do this because of the
definitions you have so carefully laid out and so strategically, AND
you provide the terms that are to be used when applying the various
results that have been proved. Those are the terms for universal
instantiations and existential generalizations. THE SOFTWARE simply
finds all of the proofs because they are in predicate calculus and
they are generally completely findable BECAUSE all of the hard work is
in the mere compilation of the right definitions and the right lemma
and theorem statements and the right TERMS to be used. THE BEAUTIFUL
thing is if this works, then the prospects for the TEXT to be FULLY
READABLE is high, because there are no proofs, yet it is completely
rigorous.
COMMENT: Of course these terms that are provided use more and more of
the defined notions that are provided.
In other words, the fully rigorous textbook looks like a totally
readable and totally uniformly illuminating, series of definitions,
lemmas, theorems, axiom quotations, and NO PROOFS. They are generated
automatically.
And it is especially friendly. you can even sugar coat it with some
English. "Of particular interest is the formation of the sets blah
blah blah", whenever you make a new definition and want to use a set
formation axiom. Or apply the mean value theorem to such and such.
HINTS WITH FRIENDLY VITAL INFORMATION.
I will try to make elementary suggestions like this, where I give this
new or "new" type of proof for some basic situations. One easy
situation to do this for is ELEMENTARY NUMBER THEORY IN PA. I think
the whole subject is very amenable to this approach where very LIMITED
VITAL INFORMATION is given and nothing even looks like a proof, yet it
is all absolutely rigorous because any decent Proof Assistant can
easily find the proofs which all of this SIMPLE VITAL INFORMATION. The
tech has the terms to play with and all of the definitions to play
with.
##########################################
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 871st 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
869: Structural Proof Theory/1 2/13/21 10:44AM
870: Structural Proof Theory/2 2/18/21 6:30PM
Harvey Friedman
More information about the FOM
mailing list