*To*: Gottfried Barrow <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] I want to print axiomatization info*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 10 Jul 2012 08:57:39 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4FFB7A8A.4060201@gmx.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>

On 10 Jul 2012, at 01:42, Gottfried Barrow wrote: > So I reduce (!R. ((P --> Q --> R) --> R)) down to > > !R. ((P /\ Q) \/ R) No need even to do that. The reasoning is very simple. let P and Q be two given formulas, and suppose that you have !R. ((P --> Q --> R) --> R). And suppose that you want to prove some formula, R say (just to keep things very simple). Then it is enough to prove P --> Q --> R. Which means, you may as well assume that P and Q are actually true while you are proving R. And that is what it means to know P&Q. Disjunction can be defined similarly. If I'm not mistaken, this discovery is due to Frege. Larry Paulson

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

**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] Annotations in Simpl
- Next by Date: Re: [isabelle] Annotations in Simpl
- 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