[FOM] 310:Thematic PA Incompleteness 2
Harvey Friedman
friedman at math.ohio-state.edu
Tue Nov 6 05:31:11 EST 2007
Here we discuss some decision procedures for some very elementary languages.
In the case of decision procedures for finite functions, the connection with
PA is this.
A. There is a decision procedure for the problem.
B. There is an algorithm which, provably in PA + 1-Con(PA), is a decision
procedure for the problem.
C. There is no algorithm which, provably in PA, is a decision procedure for
the problem.
D. I.e., PA cannot "present and verify any decision procedure for the
problem".
The following problem remains:
E. Does PA prove the existence of a decision procedure for the problem?
I suspect that the answer is yes in many cases. But this will require some
effort to establish.
In analogy with the situation in BRT = Boolean Relation Theory, Chapter 3,
we would like to provide a nice simple PROPERTY of the decidable set that
cannot be proved in PA. This we can accomplish.
1. Decision Procedures for f:N^k into N.
2. Decision Procedures for limited f:N^k into N.
3. Decision Procedures for limited f:[n]^k into [n], n large.
1. DECISION PROCEDURES FOR f:N^k into N.
We use N for the set of all nonnegative integers. Consider the template of
sentences
*) (forall f:N^k into N)(therexists v1 < ... < vr in N)(phi)
where phi is a conjunction of formulas of the form f(x1,...,xk) <=
f(y1,...,yk), where x1,...,xk,y1,...,yk are among v1,...,vr.
THEOREM 1.1. There is a decision procedure for *) which works, provably, in
RCA0 + "epsilon_0 is well ordered".
THEOREM 1.2. There is no decision procedure for *) which works, provably, in
ACA0.
THEOREM 1.3. The following is provable in RCA0 + "epsilon_0 is well
ordered", but not in ACA0. If an instance of *) is true for all recursive f,
then that instance of *) is true. The same holds if we replace "recursive"
by "elementary recursive".
THEOREM 1.4. The following is provably equivalent fo "epsilon_0 is well
ordered" over RCA0. The phi such that *) is true are closed under
conjunction.
THEOREM 1.5. Every instance of *) is either refutable in RCA0 or provable in
ACA0.
The phenomenon in Theorem 1.5 has been appearing with some frequency. E.g.,
in BRT, Chapter 3.
Now consider the richer template of sentences
**) (forall f:N^k into N)(therexists v1,...vr in N)(phi)
where phi is a propositional combination of formulas of the form
f(x1,...,xk) <= f(y1,...,yk), vi < vj, where x1,...,xk,y1,...,yk are among
v1,...,vr.
THEOREM 1.6. There is a decision procedure for **) which works, provably, in
RCA0 + "epsilon_0 is well ordered".
THEROEM 1.7. There is no decision procedure for **) which works, provably,
in ACA0.
THEOREM 1.8. The following is provable in RCA0 + "epsilon_0 is well
ordered", but not in ACA0. If an instance of *) is true for all recursive f,
then that instance of **) is true. The same holds if we replace "recursive"
by "elementary recursive".
THEOREM 1.9. Every instance of **) is either refutable in RCA0 or provable
in ACA0.
2. DECISION PROCEDURES FOR LIMITED f:N^k into N.
We say that f:N^k into N is limited if and only if for all x in N^k, f(x) <=
max(x).
Consider the template of sentences
*') (forall limited f:N^k into N)(therexists v1 < ... < vr in N)(phi)
where phi is a conjunction of formulas of the form f(x1,...,xk) <=
f(y1,...,yk), where x1,...,xk,y1,...,yk are among v1,...,vr.
THEOREM 2.1. There is a decision procedure for *') which works, provably, in
RCA0 + 1-Con(PA).
THEOREM 2.2. There is no decision procedure for *') which works, provably,
in ACA0.
THEOREM 2.3. Every instance of *') is either refutable in RCA0 or provable
in ACA0.
Now consider the richer template of sentences
**') (forall limited f:N^k into N)(therexists v1,...vr in N)(phi)
where phi is a propositional combination of formulas of the form
f(x1,...,xk) <= f(y1,...,yk), vi < vj, where x1,...,xk,y1,...,yk are among
v1,...,vr.
THEOREM 2.4. There is a decision procedure for **') which works, provably,
in RCA0 + 1-Con(PA).
THEROEM 2.5. There is no decision procedure for **') which works, provably,
in ACA0.
3. DECISION PROCEDURES FOR LIMITED f:[n]^k into [n], n LARGE.
We use [n] = {0,...,n}. We say that f:[n]^k into [n] is limited if and only
if for all x in [n]^k, f(x) <= max(x).
Consider the template of sentences
#) (for all n >> k >= 1)(forall limited f:[n]^k into [n])(therexists v1 <
... < vr in [n])(phi)
where phi is a conjunction of formulas of the form f(x1,...,xk) <=
f(y1,...,yk), where x1,...,xk,y1,...,yk are among v1,...,vr.
THEOREM 3.1. There is a decision procedure for #) which works, provably, in
EFA + 1-Con(PA). Both #) and *') are the same (the true ones have the same
phi).
THEOREM 3.2. There is no decision procedure for #) which works, provably, in
PA.
THEOREM 3.3. Every instance of #) is either refutable in EFA or provable in
PA.
Now consider the richer template of sentences
##) (for all n >> k >= 1)(forall limited f:[n]^k into [n])(therexists
v1,...,vr in [n])(phi)
where phi is a propositional combination of formulas of the form
f(x1,...,xk) <= f(y1,...,yk), vi < vj, where x1,...,xk,y1,...,yk are among
v1,...,vr.
THEOREM 3.4. There is a decision procedure for ##) which works, provably, in
EFA + 1-Con(PA). There is no decision procedure which provably works for ##)
in PA.
THEOREM 3.5. Every instance of ##) is either refutable in RCA0 or provable
in PA.
**********************************
I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 310th 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-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM. NOTE: The title of #269 has been corrected from
the original.
250. Extreme Cardinals/Pi01 7/31/05 8:34PM
251. Embedding Axioms 8/1/05 10:40AM
252. Pi01 Revisited 10/25/05 10:35PM
253. Pi01 Progress 10/26/05 6:32AM
254. Pi01 Progress/more 11/10/05 4:37AM
255. Controlling Pi01 11/12 5:10PM
256. NAME:finite inclusion theory 11/21/05 2:34AM
257. FIT/more 11/22/05 5:34AM
258. Pi01/Simplification/Restatement 11/27/05 2:12AM
259. Pi01 pointer 11/30/05 10:36AM
260. Pi01/simplification 12/3/05 3:11PM
261. Pi01/nicer 12/5/05 2:26AM
262. Correction/Restatement 12/9/05 10:13AM
263. Pi01/digraphs 1 1/13/06 1:11AM
264. Pi01/digraphs 2 1/27/06 11:34AM
265. Pi01/digraphs 2/more 1/28/06 2:46PM
266. Pi01/digraphs/unifying 2/4/06 5:27AM
267. Pi01/digraphs/progress 2/8/06 2:44AM
268. Finite to Infinite 1 2/22/06 9:01AM
269. Pi01,Pi00/digraphs 2/25/06 3:09AM
270. Finite to Infinite/Restatement 2/25/06 8:25PM
271. Clarification of Smith Article 3/22/06 5:58PM
272. Sigma01/optimal 3/24/06 1:45PM
273: Sigma01/optimal/size 3/28/06 12:57PM
274: Subcubic Graph Numbers 4/1/06 11:23AM
275: Kruskal Theorem/Impredicativity 4/2/06 12:16PM
276: Higman/Kruskal/impredicativity 4/4/06 6:31AM
277: Strict Predicativity 4/5/06 1:58PM
278: Ultra/Strict/Predicativity/Higman 4/8/06 1:33AM
279: Subcubic graph numbers/restated 4/8/06 3:14AN
280: Generating large caridnals/self embedding axioms 5/2/06 4:55AM
281: Linear Self Embedding Axioms 5/5/06 2:32AM
282: Adventures in Pi01 Independence 5/7/06
283: A theory of indiscernibles 5/7/06 6:42PM
284: Godel's Second 5/9/06 10:02AM
285: Godel's Second/more 5/10/06 5:55PM
286: Godel's Second/still more 5/11/06 2:05PM
287: More Pi01 adventures 5/18/06 9:19AM
288: Discrete ordered rings and large cardinals 6/1/06 11:28AM
289: Integer Thresholds in FFF 6/6/06 10:23PM
290: Independently Free Minds/Collectively Random Agents 6/12/06 11:01AM
291: Independently Free Minds/Collectively Random Agents (more) 6/13/06
5:01PM
292: Concept Calculus 1 6/17/06 5:26PM
293: Concept Calculus 2 6/20/06 6:27PM
294: Concept Calculus 3 6/25/06 5:15PM
295: Concept Calculus 4 7/3/06 2:34AM
296: Order Calculus 7/7/06 12:13PM
297: Order Calculus/restatement 7/11/06 12:16PM
298: Concept Calculus 5 7/14/06 5:40AM
299: Order Calculus/simplification 7/23/06 7:38PM
300: Exotic Prefix Theory 9/14/06 7:11AM
301: Exotic Prefix Theory (correction) 9/14/06 6:09PM
302: PA Completeness 10/29/06 2:38AM
303: PA Completeness (restatement) 10/30/06 11:53AM
304: PA Completeness/strategy 11/4/06 10:57AM
305: Proofs of Godel's Second 12/21/06 11:31AM
306: Godel's Second/more 12/23/06 7:39PM
307: Formalized Consistency Problem Solved 1/14/07 6:24PM
308: Large Large Cardinals 7/05/07 5:01AM
309: Thematic PA Incompleteness 10/22/07 10:56AM
Harvey Friedman
More information about the FOM
mailing list