Re: [mizar] theorems of the form "if A then T", where A is known to be independent of TG

To: mizar-forum@mizar.uwb.edu.pl
Subject: Re: [mizar] theorems of the form "if A then T", where A is known to be independent of TG
From: Josef Urban <urban@ktilinux.ms.mff.cuni.cz>
Date: Mon, 7 Jan 2008 19:43:11 +0100 (CET)



On Fri, 4 Jan 2008, Jesse Alama wrote:

Does the MML contain any statements of the form "if A then T", where A
is a statement known to be independent of Tarski-Grothendieck set
theory (TG)?

very likely anything containing the GCH predicate; there are two suchtrivial theorems in CARD_FIL


Josef

References:
- [mizar] theorems of the form "if A then T", where A is known to be independent of TG
  - From: Jesse Alama <alama@stanford.edu>