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

```On 7/9/2012 2:35 PM, Lawrence Paulson wrote:
```
```I honestly don't think doing such substitutions is of any benefit at all.
See if you can make some sense of each definition individually.
```
```
I can make sense of the logic with these equivalencies:

(A --> B --> C) == ((A /\ B) --> C), and
(A --> B) == (~A \/ B).

So I reduce (!R. ((P --> Q --> R) --> R)) down to

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

THE_SCRATCH_THIS_FUNCTION
```
(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).
```
THE_ALMOST_DID_SAY_SOMETHING_DUMB_FUNCTION__MAYBE_STILL_AM
```
(I almost sent this email off based on the above sentence. A faulty bias was causing me to misinterpret my truth table, plus my final result column was under an "/\" due to my writing.
```
```
So when R=false, the reduction above functions like conjunction. This brings to my attention to the definition
```
False == (!P. P).

```
I've gone on too long here, but I've already written what's below, so I leave it. For me, truth table logic vs. constructive and natural deduction logic 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.
```
```
If you don't read what's below, it'll be no loss, but it represents certain aspects of life, as experienced by me.
```)

```
But, though I haven't went through my natural deduction textbook much, I assume that it's saying "for every R that is asserted to be true...".
```
```
If that's the case, then the engine is somehow implementing and_def as conjunction, which, of course, I know to begin with.
```
```
It could be that I've said something dumb, so I write it with a little typing,
```
!R::('a => bool). ((P /\ Q) \/ (R::('a => bool))),

```
to try and figure out if I have said something dumb. I know that R can be viewed as a proposition, but I'm not used to quantifying over propositions; I'm used to quantifying over elements of a set, like
```
!x P(x).

```
I've gone on like this to demonstrate (even more) that I have some weaknesses in logic. I assume that your B.S. in Math at CalTech (not to mention your PhD) gave you a lot better education than my B.S. in Math at Podunk University, but I also know from experience and observation that most undergrad and graduate degrees in math don't give people much more than a basic education in logic.
```
```
Anyway, you're paying the price for giving people access to the details of the engine, unlike Mizar.
```
```
Can I work without understanding all the logic details? I suppose I have to. But if I get access to information, many times I think I'm supposed to understand it. Actually, I do need to set aside some of this low-level stuff. I'm progressing at a snail's pace.
```
GB

>
>
> On 9 Jul 2012, at 20:28, Gottfried Barrow wrote:
>
```
>> I kind of figured out that in the definitions below, I should start doing some substitutions, like
```>>
>> P&  Q == !R. ((P-->  Q-->R) -->   R)
>>       == (R = (%x.True)). ((P-->  Q-->R) -->   R)
>>       == (R = (%x.((%y::bool. y) = (%y. y))). ((P-->  Q-->R) -->   R)
>>

```
```
On 9 Jul 2012, at 20:28, Gottfried Barrow wrote:

```
```I kind of figured out that in the definitions below, I should start doing some substitutions, like

P&  Q == !R. ((P-->  Q-->R) -->   R)
== (R = (%x.True)). ((P-->  Q-->R) -->   R)
== (R = (%x.((%y::bool. y) = (%y. y))). ((P-->  Q-->R) -->   R)

```
```

```
```

```

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