# Re: [isabelle] I want to print axiomatization info

```On 7/10/2012 2:57 AM, Lawrence Paulson wrote:
```
```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.
```
```
```
I'll do the easy part and show HOL's definition of disjunction to complete the discussion.
```
P | Q  == !R.(P-->R) --> (Q-->R) --> R

Larry, thanks for the explanation of the not-so-straightforward logic.

Regards,
GB

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.