878: Structural Proof Theory/10

Wed Mar 3 20:53:40 EST 2021

I have a few additional insights into how I am proposing to
meaningfully associate integer constants to practically all
mathematical theorems. There are definitely several subtleties I did
not take into account fully or properly yet.

The goal was and is to MEANINGFULLY AND REASONABLY ROBUSTLY ASSIGN
INTEGERS to all mathematical theorems that reflects the COMPLEXITY OF
THEIR PROOF. I.e., look for the LEAST COMPLEXITY OF ANY PROOF.

I didn't say enough to really do this decently in Structural Proof
Theory/9. I need to say more.

LET US FIRST LOOK AT AN EASIER PROBLEM. ASSIGN integers to all
mathematical definitions.

At first I thought that talking about definitions of mathematical
concepts in terms of ultimate definitions in PRIMITIVE NOTATION is
wrong headed and doesn't take into account the hierarchical nature of
the DEFINITIONAL STRUCTURE of mathematics.

However, I take this back in the following sense. WE CAN TURN THIS ON
ITS HEAD. That is, think of the hierarchical definitions of
mathematics as giving UPPER BOUNDS on the complexities of DEFINITIONS
IN PRIMITIVE NOTATION. And WHY we don't get a true exponential
EXPLOSION in this sense in our mathematical concepts, is a rather
INTRIGUING question.

In the case of set theory, total number of occurrences of variables is
one crude measure that requires no explanation. So let's run with that
and see where it TAKES us.

TOY QUESTIONS

1. y = {x}. How many variable occurrences are needed in primitive
notation? (forall z)(z in y iff z = x). FIVE. Best possible???
2. z = {x,y}. How many? (forall w)(w in z iff (w = x or w = y)).
SEVEN. Best possible??
3. x containedin y. How many? (forall z)(z in x implies z in y). FIVE.
Best possible??
4. |x| = 0. How many? (forall y)(not(y in x). THREE. Best possible?
5. |x| = 1. How many? (therexists y)(y in x) and (forall y,z)(y in x
and z in x implies y = z). ELEVEN. Best possible? NO WAY.
6. |x| = 1. How many? (rherexists y)(forall z)(z in x iff z = y). SIX.
Best possible?
7. Let n be external. |x| = n. How many as a function of n? Best possible?
8. x is a transitive set. (forall y,z)(x in y and y in z implies x in
z). EIGHT. Best possible?
9. y is the power set of x. (forall z)(z in y iff (forall w)(w in z
implies w in x)). EIGHT. Best possible?
10. x is a finite set. ????????
11. x is countable. ?????????
12. x,y have the same cardinality. ????????

It is not clear to me WHAT KINDS OF PROBLEMS these are in terms of
what techniques are needed to resolve them.

QUESTION. ARE THE NATURAL OR EVEN ORIGINAL DEFINITIONS OF STANDARD
MATHEMATICAL DEFINITIONS OPTIMAL IN TERMS OF THE NUMBER OF OCCURRENCES
OF SYMBOLS? I.e. you can expand them out and get optimal definitions
in primitive notation in terms of the number of occurrences of
variables?

NOW LET'S go back to trying to assign integers to all mathematical
theorems. WE WOULD LIKE to have these numbers defined in a way that is
not tied to any special set of axioms and rules. Rather  the numbers
should reflect a fundamental state of affairs independently of human
engineering.

HERE IS ONE TO ME INTERESTING NUMBER. Let A be a theorem of
mathematics. Yes it is presented with an hierarchical set of
definitions leading up to it. Never pretty much never ever in the
primitive notation of ZFC.

Let A be an actual theorem of ZFC based on an hierarchical set of
definitions. Then there is a robust definition of A*, which is A put
into primitive notation epsilon,=. And we can define n(A) to be the
least number of occurrences of variables in some finite fragment T of
ZFC which logically implies A*.

Now there is something important to point out here. ALMOST ALWAYS, A
is goint to be provable in WZC = weak Zermelo with Choice. SINCE WZC
IS FINITELY AXIOMATIZABLE,  my n(A) is UNIVERSALLY BOUNDED by some
fixed integer M. So my n(A) could have nothing to do with A, maybe
sometimes, maybe often, maybe usually, maybe never.

I DON'T HAVE AN INTUITION ABOUT WHAT IS GOING ON HERE. This matter
seems to be VERY SERIOUSLY IMPACTED by my work in
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#112. There I give FINITELY MANY AXIOMS for NBG and also for WZC which
are limited in number and very small and exactly the kinds of axioms
you would imagine a mathematician actually using and even want to use.

So may my Downloadable #112 kills this line. OR MAYBE IT MAKES IT EVEN
BETTER!. YES!!!! or MAYBE!!!!!

Redefine n(A) as follows. Let A be an actual theorem of NBGC. Then we
know it is provable in my axiomatization T0 of NBGC that you might
learn to love. Then we know that T0 LOGICALLY IMPLIES A!!

Now we try to apply my posting #877, Structural Proof Theory/9
https://cs.nyu.edu/pipermail/fom/2021-March/022533.html here.

Thus we have the logical validity T0 implies A to do that
EXISTENTIAL/UNIVERSAL INSTANTIATION SAT SOLVER process.

##########################################

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 878th 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/24/21  12:10AM
870: Structural Proof Theory/2  2/28/21  1:18AM
871: Structural Proof Theory/3  2/28/21  9:27PM
872: Structural Proof Theory/4  2/28/21  10:38PM
873: Structural Proof Theory/5  3/1/21  12:58PM
874: Structural Proof Theory/6  3/1/21  6:52PM
875: Structural Proof Theory/7  3/2/21  4:07AM
876: Structural Proof Theory/8  3/2/21  7:27AM
877: Structural Proof Theory/9  3/3/21  7:46PM

Harvey Friedman