872: Structural Proof Theory/4

Sun Feb 28 22:38:20 EST 2021

I will now start to offer up a NEW KIND OF PROOF SYSTEM for elementary
number theory in PA made practical for this purpose.

There will be the pure logic component which stays within first order
predicate calculus with equality, and with the usual hierarchical
definition facility.

HOWEVER, we are also allowed to, part, of the definition facility,
INTRODUCE NEW FUNCTIONS AND RELATIONS not only explicitly as usual,
but also implicitly like PRIMITIVE RECURSIVE FUNCTION SYMBOLS. Only we
allow a much more flexible framework for the introduction of functions
and relations. Namely

1. Introduction of functions and relations by recursion on the natural
numbers. Primitive recursion is a special case, and we know that it
can be awkward.
2. Allow partially defined such. The functions are still defined
everywhere, but the functions and relations might not be PINNED DOWN
everywhere. LIke I may not care what the function does at 0, or I may
care only what the function does at even numbers. I.e., I could
introduce HALF by HALF(2n) = n, when I don't care what HALF(35) is.

I just want some greater flexibility because I want BEAUTIFUL
ABSOLUTELY RIGOROUS TEXT for elementary number theory that is
INCREDIBLY READABLE.

Now WHAT ARE THE RULES OF PROOF? In order to shock you I will go super
ambitious.

RULE 1. Define the relation or function F or R by blah blah blah.
RULE 2. Apply induction to blah blah blah with induction variable blah.
RULE 3. Apply such and such previous statements using the TERMS blah blah blah.

At each stage, run in the background, state of the art proof
assistants to see if everything is fully rigorous as planned.

And this can be used for MATH ED.

This idea is so clean that it should be able to drive SEMIFORMAL
investigations by hand. And with the TECH at your side, verify that
the TECH is filling in all of the details as we intend. Maybe you gave
the wrong term? Or maybe you didn't give all of the crucial terms? AND
IT IS REQUIRED THAT on the basis of these RULES, you are staying
totally within the usual first order predicate calculus with equality.

NOTE: Induction is the usual go from n to n+1. But we all know that
course of values induction is derived BUT very useful to have. So

RULE 2a. Apply course of values induction to blah blah blah with
induction variable blah.

Also maybe something needs to be said concerning UNRAVELLING
DEFINITIONS. We all know cases where we definitely NEED to unravel a
definition, only going so far though, certainly not all the way down
to primitive notation. We all know cases where we don't want to
unravel at all. I think we need

RULE 4. UNRAVEL blah blah and blah.

where it is assumed that you don't unravel unless you say to unravel.

Because of Course of Values, I have chosen to add < to the language
with the obvious axiom. DETAILS starting this SEMIFORMAL study will
begin in the next posting, SPT/5.

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

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 872nd 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
871: Structural Proof Theory/3

Harvey Friedman