[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Missing theorem

From: Leslie Lamport <tlapl...@xxxxxxxxx>
Date: Sat, 8 Nov 2014 06:46:47 -0800 (PST)
References: <35991e2d-322c-456c-adb2-2cf4653a6e90@googlegroups.com>

But this one is unprovable (automatically I mean):

ASSUME NEW S, NEW T \in S

PROVE << T >> \in S

I hope it is unprovable manually as well, since it's false. See Section 16.1.9 in Specifying Systems.

Leslie

Follow-Ups:
- Re: Missing theorem
  - From: fl

References:
- Missing theorem
  - From: fl

Prev by Date: Re: [tlaplus] Missing theorem
Next by Date: Re: Missing theorem
Previous by thread: Re: [tlaplus] Missing theorem
Next by thread: Re: Missing theorem
Index(es):
- Date
- Thread