[FOM] 166:Clean Godel Incompleteness

Harvey Friedman friedman at math.ohio-state.edu
Tue May 6 11:06:37 EDT 2003


In posting 165, I gave a version of incompleteness which avoids any 
technical hypotheses, and which tells us something rather fundamental.

Here I wish to give a version of the second incompleteness theorem 
for two rather specific very well known theories. This formulation 
seems to avoid many of the issues that have been discussed on the FOM 
recently.

I use ZC, ZFC, NBG-, and NBG.

ZC is Zermelo set theory with the axiom of choice, which is obtained 
from ZFC by dropping Replacement and Foundation.

NBG is the finitely axiomatizaed class theory of von Neumann, 
Bernays, Godel, that is closely associated with ZFC.

NBG can be finitely axiomatized. In fact, finite axiomatizations have 
surely been written down that can be easily read and understood. The 
axiomatizations do not involve arithmetization or coding in any way.

NBG- is obtained from NBG by dropping Replacement and Foundation.

THEOREM 1. Assume ZC is consistent. Then ZC does not prove that 
"there exists a nonempty set A and a binary relation R on A such that 
the relativization of every axiom of NBG- to (A,R) holds". 
Furthermore, the sentence in quotes is provable in ZFC. This proof 
can actually be displayed, and is accepted according to current 
mathematical standards as a rigorous proof in ordinary mathematics.

THEOREM 2. Assume ZFC is consistent. Then ZFC does not prove that 
"there exists a nonempty set A and a binary relation R on A such that 
the relativization of every axiom of NBG to (A,R) holds". 
Furthermore, the sentence in quotes is provable in ZFC plus the 
existence of a strongly inaccessible cardinal. This proof can 
actually be displayed, and is accepted according to current 
mathematical standards as a rigorous proof in ordinary mathematics 
under the assumption that there is a strongly inaccessible cardinal.

I am not interested here in sharp formulations, but merely in CLEAN 
formulations.

*********************************************

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.

This is the 163rd in a series of self contained postings to FOM covering
a wide range of topics in f.o.m. Previous ones counting from #100 are:

100:Boolean Relation Theory IV corrected  3/21/01  11:29AM
101:Turing Degrees/1  4/2/01  3:32AM
102: Turing Degrees/2  4/8/01  5:20PM
103:Hilbert's Program for Consistency Proofs/1 4/11/01  11:10AM
104:Turing Degrees/3   4/12/01  3:19PM
105:Turing Degrees/4   4/26/01  7:44PM
106.Degenerative Cloning  5/4/01  10:57AM
107:Automated Proof Checking  5/25/01  4:32AM
108:Finite Boolean Relation Theory   9/18/01  12:20PM
109:Natural Nonrecursive Sets  9/26/01  4:41PM
110:Communicating Minds I  12/19/01  1:27PM
111:Communicating Minds II  12/22/01  8:28AM
112:Communicating MInds III   12/23/01  8:11PM
113:Coloring Integers  12/31/01  12:42PM
114:Borel Functions on HC  1/1/02  1:38PM
115:Aspects of Coloring Integers  1/3/02  10:02PM
116:Communicating Minds IV  1/4/02  2:02AM
117:Discrepancy Theory   1/6/02  12:53AM
118:Discrepancy Theory/2   1/20/02  1:31PM
119:Discrepancy Theory/3  1/22.02  5:27PM
120:Discrepancy Theory/4  1/26/02  1:33PM
121:Discrepancy Theory/4-revised  1/31/02  11:34AM
122:Communicating Minds IV-revised  1/31/02  2:48PM
123:Divisibility  2/2/02  10:57PM
124:Disjoint Unions  2/18/02  7:51AM
125:Disjoint Unions/First Classifications  3/1/02  6:19AM
126:Correction  3/9/02  2:10AM
127:Combinatorial conditions/BRT  3/11/02  3:34AM
128:Finite BRT/Collapsing Triples  3/11/02  3:34AM
129:Finite BRT/Improvements  3/20/02  12:48AM
130:Finite BRT/More  3/21/02  4:32AM
131:Finite BRT/More/Correction  3/21/02  5:39PM
132: Finite BRT/cleaner  3/25/02  12:08AM
133:BRT/polynomials/affine maps  3/25/02  12:08AM
134:BRT/summation/polynomials  3/26/02  7:26PM
135:BRT/A Delta fA/A U. fA  3/27/02  5:45PM
136:BRT/A Delta fA/A U. fA/nicer  3/28/02  1:47AM
137:BRT/A Delta fA/A U. fA/beautification  3/28/02  4:30PM
138:BRT/A Delta fA/A U. fA/more beautification  3/28/02  5:35PM
139:BRT/A Delta fA/A U. fA/better  3/28/02  10:07PM
140:BRT/A Delta fA/A U. fA/yet better  3/29/02  10:12PM
141:BRT/A Delta fA/A U. fA/grammatical improvement  3/29/02  10:43PM
142:BRT/A Delta fA/A U. fA/progress  3/30/02  8:47PM
143:BRT/A Delta fA/A U. fA/major overhaul  5/2/02  2:22PM
144: BRT/A Delta fA/A U. fA/finesse  4/3/02  4:29AM
145:BRT/A U. B U. TB/simplification/new chapter  4/4/02  4:01AM
146:Large large cardinals  4/18/02  4:30AM
147:Another Way  7:21AM  4/22/02
148:Finite forms by relativization  2:55AM  5/15/02
149:Bad Typo  1:59PM  5/15/02
150:Finite obstruction/statisics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms, 4/22/0  5:31PM
165:Incomplelteness Reformulated  4/29/03  1:42PM

_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom


More information about the FOM mailing list