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:

074: consts
082:   All::"('a => bool) => bool" (binder "ALL " 10)

153: notation (HOL)
154:   All  (binder "! " 10)

178: defs
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 MHonArc.