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)
(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).
(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
!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
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,
> 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