879: Structural Proof Theory/11
Harvey Friedman
hmflogic at gmail.com
Thu Mar 4 04:22:23 EST 2021
1. JUMP RESEARCH
1.1. NO SQRT(2)
1.2. DIVISIBILITY
1.3. PRIME DIVISIBILITY
1.4. NO LAST PRIME
2. COMPLEXITY DEFINITION RESEARCH
2.1. WEAK COMPLEXITY
2.2. STRONG COMPLEXITY
2.3. TOY EXAMPLES/PROBLEMS
3. COMPLEXITY PROOF RESEARCH
3.1. IN PURE LOGIC
3.2. IN PA AND ZFC
SOME COMMENTS THROUGHOUT 1-3 ABOVE
before really digging in systematically in the later postings
By JUMPS I mean the JUMPS that proof assistants will definitely have
to make if they are to realize the MOST AMBITIOUS GOALS. And JUMPS
they will definitely have to make in order to get more and more
powerful on the MORE REALISTIC GOALS. We should be generating lots of
toy problems with huge mathematical challenges to meet. My general
methodology is to GO INTO THE PURE SITUATIONS where one SEVERELY
LIMITS what the TECH is given, and see what it can realistically find.
AND HOW IT DOES FIND. That way, JUMPS are seriously confronted. AND
because of the superclean pared down structure of these setups, THE
PROSPECTS FOR IMPORTANT FRUITFUL TOY PROBLEMS with tremendously
interesting THEORETICAL CHALLENGES, is maximized. NOT SO in situations
where the TECH is given everything with the kitchen sink.
WEAK COMPLEXITY refers to the crudest measure of a formula or term. It
is the total number of SYMBOLS not including parentheses. Generally
speaking, not, and, or, if then, iff, forall, therexists, variable,
constant symbol, relation symbol, function symbol, is the entire list.
Even if a constant or relation or function symbol contains an acronym
it counts as one.
STRONG COMPLEXITY refers to the measure where the numbers are
smallest. GOING ALL THE WAY, say for formulas, we could take V0 = set
of quantifier free formulas, Vn+1 = set of all propositional
combinations of formulas A, where A is obtained from some B in Vn by
putting a block of zero or more like quantifiers in front of B.
Thus STRONG COMPLEXITY in this sense is ALTERNATING QUANTIFIER DEPTH.
Of course, there is something even stronger, and that is where the
block of zero or more quantifiers are not allowed to be like
quantifiers but any quantifiers. A little hard to imagine right now
that this is going to be such a good idea.
So two notions of complexity arise for a MATHEMATICAL NOTION. One is
the least weak complexity of any of its correct definitions in
primitive notation epsilon,=. The other is the least strong complexity
of any of its correct definitions in primistive notation epsilon,=. IF
YOU LOOK AT ALL MATHEMATICAL DEFINITIONS made thus far, what can we
say about the LARGEST WEAK COMPLEXITY, and what can we say about the
LARGEST STRONG COMPLEXITY?
We all know that HIERARCHICAL definitions RULE THE DAY. So where have
they gone? Here they are REINTERPRETED as the preferred or only method
for giving UPPER BOUNDS on the weak and strong complexities of
mathematical notions.
For COMPLEXITY PROOF RESEARCH we have a difficulty right from the
start that we DON'T REALLY HAVE with COMPLEXITY DEFINITION RESEARCH.
Namely, the usual proof systems are NOT ANYWHERE NEAR ROBUST ENOUGH
for our purposes. So we invented - stealing ideas from people like
Beth, Skolem, Herbrand, Bool, and others, the approach in earlier
postings, presenting what really amounts to
*MODEL THEORETIC REFUTATIONS OF SENTENCES IN PURE LOGIC*
where we start by putting the given sentence into prenex form by the
standard algorithm, and then applying Henkin existential and universal
instantiation, and then doing a SAT problem on an infinite set of
disjunctions of literals, looking for "no SAT solution". The
complexity of the refutation is based on the minimum complexity of any
finite subset of the infinite SAT problem that has no SAT solution.
This is a very very very powerful proof system, this MODEL THEORETIC
REFUTATION system. And so what happens to all of the usual proof
systems? THEY BECOME PROOFS OF UPPER BOUNDS ON THE COMPLEXITY ARISING
IN THIS MODEL THEORETIC REFUTATION approach.
THESE IDEAS suggest many interrelated ways of associating INTEGERS to
mathematical theorems.
1. Most crudely. Look for the least possible complexity of a finite
fragment of ZFC that logically proves your mathematical theorem B.
Several complexity measures here may be appropriate. We can start with
our weak and strong complexity measures we discussed above. Under the
weak complexity measure, the actual understandable proofs of B would
supply probably rather large numbers because it would supply even a
rather large finite fragment of ZFC used in the proof. And it would be
subject to likely large variations according to who is doing the
proofs even if by normal mathematical standards they are formalizing
the same proof. This also appears to run up against these UNIVERSAL
INSTANCES of the ZFC axioms using NORMAL FORM TECHNIQUES. Having said
that, however, any kind of normal form for this purpose is likely to
be rather large. And this inexorably leads us to the STRONG complexity
measures.
So one thing right away would be to take the STRONG COMPLEXITY of the
finite fragments of ZFC that are sufficient to prove your mathematical
theorem.
CONSTANT OF MATHEMATICAL NATURE?? THE LEAST INTEGER n SUCH THAT ALL
PROVED MATHEMATICAL THEOREMS (FROM ZFC) ARE LOGICALLY IMPLIED BY A
FINITE FRAGMENT OF ZFC OF STRONG COMPLEXITY AT MOST n.
Still NOT SURE whether I have quite set this up right so as to
generate the right kind of TOY examples and TOY challenges.
##########################################
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
878: Structural Proof Theory/10
Harvey Friedman
More information about the FOM
mailing list