Re: [isabelle] I want to print axiomatization info



I imagine that the following paper (Church, 1940) has all the information you need:

http://www.classes.cs.uchicago.edu/archive/2007/spring/32001-1/papers/church-1940.pdf

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
> defs
>  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.