From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/1099 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: incompleteness of ZF Date: Sat, 3 Apr 1999 17:12:29 +0200 (MESZ) Message-ID: <199904031512.AA079642350@fb0448.mathematik.tu-darmstadt.de> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241017566 29509 80.91.229.2 (29 Apr 2009 15:06:06 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:06:06 +0000 (UTC) To: CATEGORIES@mta.ca Original-X-From: cat-dist Tue Apr 6 06:03:11 1999 Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id EAA28995 for categories-list; Tue, 6 Apr 1999 04:36:25 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Mailer: ELM [version 2.4ME+ PL47 (25)] Original-Sender: cat-dist@mta.ca Precedence: bulk Original-Lines: 26 Xref: news.gmane.org gmane.science.mathematics.categories:1099 Archived-At: Dear Paul, a short reply to your mail about inconsistency of replacement. As Paul has already remarked in his mail the type-theoretic counterpart of replacement is that of universe `a la Martin-Loef. As in case of replacement the use of universes is that they allow for construction of families of types (as e.g. needed for inverse limit constructions in Domain Theory which cannot be performed in pure topos logic precisely for this reason). But as already observed in a survey article by Thierry Coquand (ftp://ftp.cs.chalmers.se/users/cs/coquand/meta.ps.Z) and, surely, known to Martin-Loef himself it holds that in type theory with n+1 universes one may prove the consistency of type theory with n universes simply by constructing a model using the n+1st universe. But, of course, this extra universe is needed for the consistency proof. Accordingly, one cannot prove the consistency of type theory with $\omega$ universes without postulating an $\omega$th universe. Quite the same phenomenon is going on in set theory as already pointed out by some previous replies. However, in set theory due to the presence of ``impredicative'' axioms the proof theoretic strength is incredibly stronger than set of Martin-Laoef type theory with $\omega4 universes. Best, Thomas