*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] I want to print axiomatization info*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Wed, 11 Jul 2012 07:54:19 -0500*In-reply-to*: <4FFBD64D.5030407@in.tum.de>*References*: <4FF8DFF9.4040304@gmx.com> <9BD4C787-4163-4D60-A87F-D7285EE940DF@cam.ac.uk> <4FF9AA7E.4020902@gmx.com> <10A31E58-2DD6-4D38-B4DF-789080095575@cam.ac.uk> <4FFB30C1.1090504@gmx.com> <E52CDD57-A77A-49F5-B981-C86AD230EA5D@cam.ac.uk> <4FFB7A8A.4060201@gmx.com> <4FFBD64D.5030407@in.tum.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 7/10/2012 2:14 AM, Lars Noschinski wrote:

So I reduce (!R. ((P --> Q --> R) --> R)) down to !R. ((P /\ Q) \/ R)This would be "!R. (~(P /\ Q) \/ R)"

I don't know. This is what I get: (P --> Q --> R) --> R == ((P /\ Q) --> R) --> R) == (~(P /\ Q) \/ R) --> R) == ~(~(P /\ Q) \/ R) \/ R == ((P /\ Q) /\ ~R) \/ R == ((P /\ Q) \/ R) /\ (~R \/ R) == (P /\ Q) \/ R

So when R=false, the reduction above functions like conjunction. This brings to my attention to the definition False == (!P. P)."!P. P" just says "all propositions hold". As long as our logic is consistent, this is not going to be the case, so we choose this as our value for False.

!R. ((P /\ Q) \/ R), or even !R. (~(P /\ Q) \/ R).

conj P Q,

With !R. ((P /\ Q) \/ R),

"For every proposition R, (P /\ Q) is true or R is true." A more friendlier statement would be this, using your statement above: "Every proposition is true or (P /\ Q) is true". I guess that's it. Simple stuff, unless it's not. Thanks for the help. Regards, GB

**Follow-Ups**:**Re: [isabelle] I want to print axiomatization info***From:*Lars Noschinski

**References**:**[isabelle] I want to print axiomatization info***From:*Gottfried Barrow

**Re: [isabelle] I want to print axiomatization info***From:*Lawrence Paulson

**Re: [isabelle] I want to print axiomatization info***From:*Gottfried Barrow

**Re: [isabelle] I want to print axiomatization info***From:*Lawrence Paulson

**Re: [isabelle] I want to print axiomatization info***From:*Gottfried Barrow

**Re: [isabelle] I want to print axiomatization info***From:*Lawrence Paulson

**Re: [isabelle] I want to print axiomatization info***From:*Gottfried Barrow

**Re: [isabelle] I want to print axiomatization info***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] Nice representation for access to maps
- Next by Date: Re: [isabelle] I want to print axiomatization info
- Previous by Thread: Re: [isabelle] I want to print axiomatization info
- Next by Thread: Re: [isabelle] I want to print axiomatization info
- Cl-isabelle-users July 2012 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