[FOM] 329: Finite Decidability/Templating

Harvey Friedman friedman at math.ohio-state.edu
Fri Jan 16 15:55:42 EST 2009

For many years, we have been emphasizing decidability investigations  
of an unusual kind.

The normal context for decidability results is where you have an  
infinite family of discrete objects, and you want an algorithm for  
determining membership - or a proof that no such algorithm exists.

In Finite Decidability, the family of discrete objects is finite.

Of course, under the usual notion of decidability, any finite family  
is decidable. But two important issues remain. One is algorithmic, and  
the other is proof theoretic.

1. Algorithmic. If the number of elements of the finite family is  
reasonable, so that we can actually construct the table of elements,  
then there are no (obvious) algorithmic issues remaining, once that  
table has been constructed. Algorithmic issues enter when we cannot  
feasibly construct the table of elements. So assume that a table is  
not feasible.

We can ask that the finite decision procedure be efficient, in the  
sense of the amount of time and memory involved. To attempt to make  
this rigorous, we make use of an appropriate theory of finite RAMs. Of  
course, many robustness issues need to be addressed.

2. Proof theoretic. There is an immediate conclusion that we can draw  
about the finite family S, from having a decision procedure for  
membership in S - regardless of the size of S and how efficient the  
algorithm is. We do have to assume that we have proved in ZFC that  
some particular decision procedure works. We can conclude,  
automatically, that

every statement in S is provable or refutable in ZFC.

In general, we will have a proof that the decision procedure works  
within a system T, which may or may not be much weaker than ZFC. Then  
we immediately conclude that

every statement in S is provable or refutable in T.


We have published a clear cut case of this - namely, the sentences of  
set theory in epsilon,=, in forall, therexists, not,and,or,implies,  
with at most 3 quantifiers. These can be put into prenex form

(Q_1 x)(Q_2 y)(Q_3 z)(A(x,y,z))

where A is quantifier free in x,y,z,epsilon,=. There are 18 atomic  
formulas. Only 12 need be considered. Up to tautological equivalence,  
there are 2^2^12 = 2^4096 A's. THe total number of sentences to be  
considered is then 2^4099. However, the sentences and their negations  
are in this count, and so the adjusted count is 2^4098. See

H. Friedman, Three quantifier sentences, Fundamenta Mathematicae, 177  
(2003), 213-240

for our treatment of this family. In this case, a major Corollary of  
the investigation is that

every 3 quantifier sentence in set theory is provable or refutable in  
(a weak fragment of) ZF.

An example where the number of elements fits into a table, is the  
subject of Chapter 3 in

H. Friedman, Boolean Relation Theory and Incompleteness, Chapter 3, http://www.math.ohio-state.edu/%7Efriedman/manuscripts.html

The main set here has 6561 elements, although we actually consider an  
expanded set with 32,805 elements. Their is an obvious symmetry of  
size 12 (though some equivalence classes have fewer than 12 elements),  
which cuts this down to 574 for the basic set, and 2,870 for the  
extended set. These appear in the actual table in section 3.14.

The main Corollaries of the table ares:

Every one of the 6561 or even 32,805 statements can be proved or  
refuted in ZFC augmented with strongly Mahlo cardinals of every finite  
Aside from some specific group of 12 of these statements, they can all  
be proved or refuted in RCA_0.


We now come to another aspect and application of Finite Decidability.  
In recognition of its strategic value, we call this Templating.

The need for templating became clear to us because we have  
consistently, over the years, run up against the following situation.

We construct examples of statements that are independent of certain  
formal systems, which are in certain focused mathematical contexts,  
and exhibit various degrees of "naturalness". We make a lot of  
progress in simplifying them, and go as far as we can imagine without  
a substantial change of context. HOWEVER, typically, there is still an  
element of ad hoc choice in the exact details of the statement. These  
details may be immediately digestible, but still there remains the  
question of justification the exact choice of details.

ENTER TEMPLATING!! We try to make progress by

parameterizing our way out of this situation.

We try to introduce parameters representing the ad hoc choices made in  
the details of the independent statement.

The idea is to then "replace" the independent statement with the new  
family of statements, of which the original independent statement is  
an element.

Normally, the resulting *set of statements* is considerably less ad  
hoc than the *original element*.

In practice, some difficulties arise.

i. The resulting set of statements itself has ad hoc features. These  
can be considerably reduced by a number of methods, generally in  
combination. One is to recast the original independent statement in  
somewhat different terms, which may lend themselves to easier and more  
natural templating. Sometimes this process suggests a somewhat new  
independence result, which requires new ideas.

ii. The other method, used in combination with i, is to expand the  
scope of the statements. This often gets rid of ad hoc elements in the  
templates. Larger, more inclusive templates, generally tend to be less  
ad hoc - and obviously more striking.

iii. BUT, even modest templates are extremely hard to analyze. If you  
look at what is involved in the full blown treatment of the templating  
discussed above that I have done - you see that this is not easy to  
pull off. However, I do find it very rewarding - after completion.


I am convinced that Templating is here to stay as an integral part of  
the expansion of Incompleteness.

In fact, I have conjectured that the whole of mathematics will  
advantageously become templated, with independence results of ZFC  
becoming commonplace.

A discussion of this vision for the future can be seen in

H. Friedman, My Forty Years on His Shoulders. Horizons of Truth,  
Proceedings of the Goedel Centenary, Cambridge University Press. To  
appear, 2009. http://www.math.ohio-state.edu/%7Efriedman/manuscripts.html 
  Preprints, Abstracts, Drafts, manuscript #58.

in section 12, where we write:

"Every interesting substantial mathematical theorem can be recast as  
one among a natural finite set of statements, all of which can be  
decided using well studied extensions of ZFC, but not all of which can  
be decided within ZFC itself."

In the next numbered posting, #330, we will discuss the Templating  
process applied to the Pi01 independence results that were presented  
in #326, http://www.cs.nyu.edu/pipermail/fom/2008-October/013161.html

Also be apply Templating to the recent Polynomial Independence results  
of #328.


I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 329th 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
291: Independently Free Minds/Collectively Random Agents (more)  6/13/06
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
310: Thematic PA Incompleteness 2  11/6/07  5:31AM
311: Thematic PA Incompleteness 3  11/8/07  8:35AM
312: Pi01 Incompleteness  11/13/07  3:11PM
313: Pi01 Incompleteness  12/19/07  8:00AM
314: Pi01 Incompleteness/Digraphs  12/22/07  4:12AM
315: Pi01 Incompleteness/Digraphs/#2  1/16/08  7:32AM
316: Shift Theorems  1/24/08  12:36PM
317: Polynomials and PA  1/29/08  10:29PM
318: Polynomials and PA #2  2/4/08  12:07AM
319: Pi01 Incompleteness/Digraphs/#3  2/12/08  9:21PM
320: Pi01 Incompleteness/#4  2/13/08  5:32PM
321: Pi01 Incompleteness/forward imaging  2/19/08  5:09PM
322: Pi01 Incompleteness/forward imaging 2  3/10/08  11:09PM
323: Pi01 Incompleteness/point deletion  3/17/08  2:18PM
324: Existential Comprehension  4/10/08  10:16PM
325: Single Quantifier Comprehension  4/14/08  11:07AM
326: Progress in Pi01 Incompleteness 1  10/22/08  11:58PM
327: Finite Independence/update
328: Polynomial Independence 1

Harvey Friedman

More information about the FOM mailing list