895: Provably Recursive Functions and Sigma02
Harvey Friedman
hmflogic at gmail.com
Mon Sep 27 01:21:04 EDT 2021
The following is well known.
THEOREM 1. Suppose A is a true Pi01 sentence. Then the provably
recursive functions of PA + A are the same as the provably recursive
functions of PA.
Proof: Let A be as given. Let A = (forall n)(f(n) = 0), where f is
primitive recursive. Now let PA + A prove that phi_e is total, where
phi_e is total. We find e' such that PA proves that phi_e' is total,
where phi_e = phi_e'. phi_e' is executed at n as follows.
Run phi_e(n). If the stage of computation is t where t is greater than
some r' with f(t') not= 0, then return 0.
Note that (forall n)(f(n) = 0) is true, and so this phi_e' = phi_e.
Now arguing in PA, we see that if (forall n)(f(n) = 0) then phi_e =
phi_e' is total, and also if not(forall n)(f(n) = 0) then phi_e' is
total. Hence PA proves that phi_e' is total. QED
We now extend this to Sigma02. If the Sigma02 sentence i(therexists
n)(forall m)(f(n,m) = 0) is true then (forall m)(f(n,m) = 0) implies
it, and is a true Pi01 sentence. Therefore the provably recursive
functions of PA + (forall m)(f(n,m) = 0) i are the same as the
provably recursive functions of pA, and therefore the same as the
provably recursive functions of PA + i(therexists n)(forall m)(f(n,m)
= 0).
What remains to be seen is what happens with the case of a false
Sigma02 sentence (therexists n)(forall m)(f(n,m) = 0).
Let W_1,W_2,... be the canonical omega sequence of functions cofinal
through the provably recursive functions of PA, according to the
Wainer hierarchy. Let W(n) = Wn(n).
THEOREM 2. Suppose A is a Sigma02 sentence where PA + A is consistent.
Then W is not a provably recursive function of PA + A.
Proof: Let A be as given. We can write A in the form "phi_e is not
total". Suppose PA + A proves W is total. Then PA proves phi_e is
total or W is total. We define partial recursive f as follows. To
compute f(r), run phi_e and W simultaneously at r. Whichever halts
first use that output as the output. (break ties in favor of phi_e).
Then PA proves that f is total. I.e., f is a provably recursive
function of PA. Because of the provable dominance of W, PA proves that
phi_e is eventually f. In particular, PA proves that phi_e is total.
Hence PA + A is inconsistent, contradicting the hypothesis. QED
This result begs to be properly refined. We leave this to subscribers to
1. Replace PA and W by general systems and diagonal functions..
2. Strengthen Theorem 2 fundamentally.
##########################################
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 895th 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 3/3/21 8:53PM
879: Structural Proof Theory/11 3/4/21 4:22AM
880: Tangible Updates/1 4/15/21 1:46AM
881: Some Logical Thresholds 4/29/21 11:49PM
882: Logical Strength Comparability 5/8/21 5:49PM
883: Tangible Incompleteness Lecture Plans 5/16/21 1:29:44
884: Low Strength Zoo/1 5/16/21 1:34:
885: Effective Forms 5/16/21 1:47AM
886: Concerning Natural/1 5/16/21 2:00AM
887: Updated Adventures 9/9/21 9:47AM 2021
888: New(?) kinds of questions 9/9/21 12:32PM
889: Generating r.e. sets 9/12/21 3:38PM
890: Update on Tangible Incompleteness 9/18/21 9:50AM :
891: Remarks on Reverse Mathematics/1 9/21/21 12:50AM :
892: Remarks on Reverse Mathematics/2 9/21/21 8:37AM :
893: Remarks on Reverse Mathematics/3 9/23/21 10:04PM
894: Update on Tangible Incompleteness/2 9/25/21 2:51AM
Harvey Friedman
More information about the FOM
mailing list