Re: [isabelle] I want to print axiomatization info
On 7/10/2012 2:31 AM, Ramana Kumar wrote:
I can make sense of the logic with these equivalencies:
(A --> B --> C) == ((A /\ B) --> C), and
(A --> B) == (~A \/ B).
Sure, but you should remember that from the perspective of defining the
connectives, the definitions are primary and we would derive these
equivalences as consequences. So it would be good to get a little
intuitive appreciation for the definitions directly.
I kind of understood that I'm getting circular, which is why I wasn't so
ready to be satisfied with those kind of substitutions, but Larry told
me to forget about low-level substitutions, so that relieved me of a
feeling of responsibility to not get circular.
Larry's explanation was able to explain the logic and still only use "-->".
So I reduce (!R. ((P --> Q --> R) --> R)) down to
!R. ((P /\ Q) \/ R)
Can you see why this is a good definition for 'and'?
It's a good definition if you only have "!" and "-->" at your disposal.
It's doesn't sync up well with simplistic lessons in logic as given in
"Discrete Mathematics" by Rosen, or many other mathematical logic
textbooks. But yea, it looks good.
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
Surely when R is false but P and Q are true the result is true...?
Truth tables still work for propositional logic embedded in HOL.
You're asking about what I said there? That was messed up. I left it in
to show how I was messed up, but it leaving it in and not working to
redo the email right was probably messed up too.
The result with truth tables is the same, but there are subtle or
not-so-subtle differences in the logic notation and the use of logic
formulas as specifically used in a proof assistant. Or maybe there's
not. It could just be information overload that throws me off, which
results in me not being able to process simple statements.
...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.
Don't get confused by its being a capital letter. Look at the type. P is
a plain old boolean proposition. It doesn't take any arguments. The
definition of false basically says both boolean values are true, that
is, there is an inconsistency.
Sometimes a formula can be so simple that a newbie doesn't know how to
get information out of it. It helps for people to tell me exactly how to
phrase the meaning of a formula in informal English, until I get good at
creating my own interpretive phrases.
!R::('a => bool). ((P /\ Q) \/ (R::('a => bool))),
Surely that did not typecheck.
Here are some pertinent lines from ~/HOL/HOL.thy:
082: All::"('a => bool) => bool" (binder "ALL " 10)
153: notation (HOL)
154: All (binder "! " 10)
180: All_def: "All(P) == (P = (%x. True))"
I put this in jEdit, and it shows R::bool:
lemma "!R. (P-->Q-->R) --> R"
So, you're right, though I thought you had to be wrong, until the goal
for the proof step told me you're right. This is where things like
declare[[show_types=true]] save us a bunch of time.
It appeared to me, by line 82, that "All" takes a "('a => bool)" and
returns a bool. It could be that "All(P)" is not the same thing as "All P".
This archive was generated by a fusion of
Pipermail (Mailman edition) and