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

*From*: jack malkovick <sillymouse333@xxxxxxxxx>*Date*: Wed, 30 Nov 2022 01:11:06 -0800 (PST)*References*: <904caba2-762e-49a2-bea5-1dc6a3506929n@googlegroups.com> <498A9107-441B-4AA3-A9B1-F23E27AFAD86@gmail.com>

Yes, it makes sense, I tried that too before...

I guess I was looking for a way to formulate a theorem in such a way it will be unprovable having an inconsistent set of facts.

Would that make any sense?

On Wednesday, November 30, 2022 at 11:04:37 AM UTC+2 Stephan Merz wrote:

Hi,could you explain why you are surprised? The theorem holds for two reasons: (i) the assertion (TRUE) is trivial, and (ii) the assumptions are contradictory, as you say. From contradictory assumptions, anything can be proved, and in fact the following also passes:THEOREM

ASSUME

NEW P(_),

\A p : P(p),

\A p : ~P(p)

PROVEFALSE

OBVIOUS

Regards,

StephanOn 30 Nov 2022, at 09:53, jack malkovick <sillym...@xxxxxxxxx> wrote:I just started reading about TLAPS and I tried for fun the followingsillythingTHEOREM T ==

ASSUME

NEW P(_),

\A p : P(p),

\A p : ~P(p)

PROVE

TRUE

PROOF

OBVIOUSTo my surprise, the result was green. I hoped that somehow it would "detect" the contradictions in the assumptions.--

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/904caba2-762e-49a2-bea5-1dc6a3506929n%40googlegroups.com.

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a244225f-f9a0-4db7-894c-cf52fd0bd762n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Simple contradiction proof***From:*Stephan Merz

**References**:**[tlaplus] Simple contradiction proof***From:*jack malkovick

**Re: [tlaplus] Simple contradiction proof***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Simple contradiction proof** - Next by Date:
**Re: [tlaplus] Simple contradiction proof** - Previous by thread:
**Re: [tlaplus] Simple contradiction proof** - Next by thread:
**Re: [tlaplus] Simple contradiction proof** - Index(es):