Re: [isabelle] I want to print axiomatization info


Thanks for link to the document. I added Church's journal article to my library of HOL documents.

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)

Using trial and error, I finally decided I don't know what the notation means enough to continue to make substitutions.

If I was formally enrolled in a course, I would go and impose myself on my professor, and take up his or her time. But I'm not, so it'll have to be delayed gratification.


On 7/8/2012 1:12 PM, Lawrence Paulson wrote:
I imagine that the following paper (Church, 1940) has all the information you need:

However, Isabelle's formalism includes a much richer variety of types, including type variables and type constructors. As I recall, essentially the same system of axioms is used in HOL.

Larry Paulson

On 8 Jul 2012, at 16:42, Gottfried Barrow wrote:

I might could eventually figure out the reasoning behind your defs in HOL.thy, like for these:

LINE: 178 of src/HOL/HOL.thy
  True_def:     "True      == ((%x::bool. x) = (%x. x))"
  All_def:      "All(P)    == (P = (%x. True))"
  Ex_def:       "Ex(P)     == !Q. (!x. P x -->  Q) -->  Q"
  False_def:    "False     == (!P. P)"
  not_def:      "~ P       == P-->False"
  and_def:      "P&  Q     == !R. (P-->Q-->R) -->  R"
  or_def:       "P | Q     == !R. (P-->R) -->  (Q-->R) -->  R"
  Ex1_def:      "Ex1(P)    == ? x. P(x)&  (! y. P(y) -->  y=x)"

I'm thinking that parts of your "Interactive Proof with Cambridge LCF" and your "The Foundation of a Generic Theorem Prover" will eventually help me out, that you directly implement into HOL.thy some of the logic definitions in your LCF book. It'll take time for me to find that out.

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