873: Structural Proof Theory/5
Harvey Friedman
hmflogic at gmail.com
Mon Mar 1 12:58:29 EST 2021
ELECTRONIC TEXTBOOK DESIGN
So I am going to make some concrete suggestions for a text on
elementary number theory which is FORMALLY RIGOROUS and totally
READABLE and UNDERSTANDABLE and useful EDUCATIONALLY.
AN IMPORTANT BONUS: along the way a whole host of systematically
constructed new THEORETICAL questions will be offered. I CONJECTURE
that these questions will prove interesting, in that some can be
solved, and the solutions should be interesting. This will probably
take some serious EXPERIMENTATION, however, tgo find the right kind of
theoretical questions that are fruitful and illuminating.
STARTING POINT. I was trying to decide on whether to start with just
0,S, or whether to start with just 0,S, or best to start with 0,S,<.
The issue is this. It is clear that < is going to play a special role
very early on, and to take < as just one of a variety of inductively
defined relations makes it somewhat unnatural to pick it out for
special use (think course of values induction and least number
principle). So I decided to take as primitives, all three: 0,S,<.
So starting axioms are just these: not(Sx = 0). Sx = Sy implies x = y.
x < Sy if and only if x < y or x = y. not(x < 0).
RULES. First order logic in an ever expanding language. Language
expands because the introduction of function and relation symbols for
hierarchically. These are introduced either just by explicit
definition over previous ones introduced, along with are stating
0,<,S, or introduced by recursion. We probably want some flexibility
by what kind of recursions are allowed here. Adhering strictly to
primitive recursion is probably too rigid.
MORE RULES. Ordinary induction for any formula, course of values
induction for any formula, least number principle for all formulas.
TREATMENT OF <,S,=
A nice elemental beginning. Define >, <=, >=,not= by explicit definition.
We definitely want to start off pinning down all of the obvious
concerning =,S,<,<=,>,>=,not(=).
We immediately have a not uninteresting situation. What do we need to
prove the basic facts about < and for that matter, what are these
basic facts? Maybe we want to prove enough basic facts so that all
first order sentences in S,<,= follow logically from the finite ones
we call basic??
So we have:
1. not(Sx = 0).
2. Sx = Sy implies x = y.
3. x < Sy iff x < y or x = y.
We need to prove the following theorems.
4. x not= 0 implies there exists y such that Sy = x.
5. < is a strict linear ordering with least element 0
We know from QUANTIFIER ELIMINATION that this is complete. The first
three of these are axioms.
THEOREM 1. x not= 0 implies there exists y such that Sy = x.
Proof: OIH: x not= 0 implies there exists y such that Sy = x. OIV: x. QED
Here OIH is read "ordinary induction hypothesis". And OIV is read
"ordinary induction variable".
Let's see if this really is a complete proof in the sense I have been
talking about. Look at
0 not= 0 implies there exists y such that Sy = 0
(x not= 0 implies there exists y such that Sy = x) implies
(Sx not= 0 implies there exists y such that Sy = Sx)
which any pure logic prover can do instantly using the axioms.
CRUDE THEORY QUESTION. We have proved Theorem 1 using an OIH with an
existential quantifier. Can we use no quantifiers? Can we use one or
more universal quantifiers instead?
We want to get that < is a strict linear ordering with obvious properties.
i. not(x < x)
ii. x < y implies not(y < x)
iii. x < y and y < z implies x < z
CRUDE QUESTIONS: What kind of inductions are needed to prove which of these?
NEXT posting I want to address an important issue, namely HOW DO WE
WANT TO SCALE THIS UPWARD? We need to develop a good theory of PURE
LOGIC PROOFS based on restrictions that correspond to a GENERALLY
RECOGNIZED NOTION OF SELF PROVING. So the job of the EXPOSITOR is to
reduce everything down to FORMALLY STATED INSTRUCTIONS to the Proof
Assistant that is clearly understandable to the author and that are
FUNDAMENTALLY INTERESTING RESTRICTIONS on provability in pure logic.
SO THE AUTHOR KNOWS WHAT IS HAPPENING UNDER THE HOOD at all times.
##########################################
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 873rd 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
872: Structural Proof Theory/4
Harvey Friedman
More information about the FOM
mailing list