[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
order.
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
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
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