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.

Thanks for your time,
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.