[FOM] New Foundations consistency problem

[T.Forster at dpmms.cam.ac.uk]

   I think he wants to get it into an easily readable form before he goes 
public, and i also think that that is probably a good idea. Only paid-up 
NFistes have the stomach for it in its present form, believe me. Once he 
has the right data structures for describing the construction rigorously he 
will have something that normal people might want to read and, at that 
point, one can start thinking about machine verification. I am putting out 
feelers to see if i can get funding for a Ph.D. student to do a formal 
verification in Isabelle or HOL, but that's more than just months away.

I suppose Holmes could be answering these queries himself, but i don't want 
him distracted by correspondence!

On Oct 27 2013, David Roberts wrote:

> Ideally he would release it to the public, to get more eyes on it, and 
> hopefully generate as much interest (at least among logicians and set 
> theorists, and interested onlookers) as the recent Polymath8 project 
> centred on Zhang's recent proof of the existence of bounded gaps between 
> primes did. Holmes will get no less credit for doing so, and the field 
> would receive spin-off benefits arising from increased visibility and 
> discussion among the wider mathematical community.
>
>David Roberts
>
>On 24/10/2013, at 4:48 PM, <T.Forster at dpmms.cam.ac.uk> wrote:
>
>> Randall Holmes has a proof of Con(NF). It's a very complex object, and 
>> he redesigns it every now and then with a view to making the 
>> construction clearer, so it's very much a moving target. My Ph.D. 
>> students and i are gradually working our way through it. The view here 
>> is that it is all true, but it's going to be months before we're 
>> confident that we are on top of it.
>> 
>> 
>> On Oct 24 2013, Alasdair Urquhart wrote:
>> 
>>> I wonder if anybody could tell me the current status
>>> of the consistency problem for NF?
>>> 
>>> 
>>> _______________________________________________
>>> FOM mailing list
>>> FOM at cs.nyu.edu
>>> http://www.cs.nyu.edu/mailman/listinfo/fom
>>> 
>> _______________________________________________
>> FOM mailing list
>> FOM at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>_______________________________________________
>FOM mailing list
>FOM at cs.nyu.edu
>http://www.cs.nyu.edu/mailman/listinfo/fom
>