*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 11:49:31 -0500*In-reply-to*: <CAMej=27v47JN7ibM0P=PA1m1uift_oAmHmSvd-rn+ehgQznvng@mail.gmail.com>*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> <CAMej=27v47JN7ibM0P=PA1m1uift_oAmHmSvd-rn+ehgQznvng@mail.gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 7/10/2012 2:31 AM, Ramana Kumar wrote:

I can make sense of the logic with these equivalencies: (A --> B --> C) == ((A /\ B) --> C), and (A --> B) == (~A \/ B).Sure, but you should remember that from the perspective of defining the connectives, the definitions are primary and we would derive these equivalences as consequences. So it would be good to get a little intuitive appreciation for the definitions directly.

Larry's explanation was able to explain the logic and still only use "-->".

So I reduce (!R. ((P --> Q --> R) --> R)) down to !R. ((P /\ Q) \/ R)Can you see why this is a good definition for 'and'?

This is where my truth-table-indoctrinated mentality starts to cause me a lot of insecurity, because when R=F, P=T, and Q=T, the result is false).Surely when R is false but P and Q are true the result is true...? Truth tables still work for propositional logic embedded in HOL.

...causes me some confusion, on how to interpret a simple statement like "!P. P", or maybe, as I say below, it's because I'm not used to quantifying over propositions, but only over elements of a set, such as in "!x P(x)". I'll get straightened out with the right books.Don't get confused by its being a capital letter. Look at the type. P is a plain old boolean proposition. It doesn't take any arguments. The definition of false basically says both boolean values are true, that is, there is an inconsistency.

!R::('a => bool). ((P /\ Q) \/ (R::('a => bool))),Surely that did not typecheck.

Here are some pertinent lines from ~/HOL/HOL.thy: 074: consts 082: All::"('a => bool) => bool" (binder "ALL " 10) 153: notation (HOL) 154: All (binder "! " 10) 178: defs 180: All_def: "All(P) == (P = (%x. True))" I put this in jEdit, and it shows R::bool: lemma "!R. (P-->Q-->R) --> R"

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

- Previous by Date: Re: [isabelle] I want to print axiomatization info
- 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