*To*: John Munroe <munddr at gmail.com>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Proving consistency*From*: Benedikt N <bnord01 at googlemail.com>*Date*: Thu, 19 Aug 2010 17:17:07 +0200*In-reply-to*: <AANLkTikkpzcqM6gEYuN7Usp-1wovvAbMPE-rF64O2_Ys@mail.gmail.com>*References*: <AANLkTikkpzcqM6gEYuN7Usp-1wovvAbMPE-rF64O2_Ys@mail.gmail.com>*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 6.1; de; rv:1.9.2.8) Gecko/20100802 Lightning/1.0b2 Mnenhy/0.8.3 Thunderbird/3.1.2

Am 19.08.2010 16:50, schrieb John Munroe:

What is the theorem for proving that A is consistent? On paper, I'd like to show that I can't prove False from A, but how can that be done in practice?

In this case simply proving that there exists an instance of A.

And thereby proving that Isabelle is inconsistent.

Benedikt

**References**:**[isabelle] Proving consistency***From:*John Munroe

- Previous by Date: Re: [isabelle] stuck on proof
- Next by Date: Re: [isabelle] Proving consistency
- Previous by Thread: [isabelle] Proving consistency
- Next by Thread: Re: [isabelle] Proving consistency
- Cl-isabelle-users August 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list