RE: type bool. I think BOOL_CASES_AX can be derived from choice.
There's a topos-flavoured proof (due to Diaconescu?) in Lambek and Scott,
which I think John ported to HOL-Light.
Konrad.
On Sun, Mar 16, 2014 at 7:25 PM, Bill Richter <rich...@math.northwestern.edu
> wrote:
> I'm trying to understand Tom Hales's compact description of HOL Light in
> his AMS Notices article www.ams.org/notices/200811/tx081101370p.pdf
> The first things I don't understand are the type bool and the
> beta-conversion inference rule.
>
> Isn't there an axiom that there are exactly two term type bool, T and F,
> both constants? I can't see where Tom says that, or where it's explained.
> Maybe this is the theorem EXCLUDED_MIDDLE from class.ml. I saw in
> bool.ml something else Tom didn't explain, which Michael N explained to
> me some time ago, how to define the universal quantifier:
>
> let FORALL_DEF = new_basic_definition
> `(!) = \P:A->bool. P = \x. T`;;
>
> That's pretty close to how Church defined the universal quantifier in his
> 1940 paper A Formulation of the Simple Theory of Types
> http://www.jstor.org/stable/2266170, with his primitive constant Pi.
> Church gives beta-conversion as an inference rule, and I think that's
> what HOL4 does as well. Here's from p 26 of LOGIC;
>
> http://sourceforge.net/projects/hol/files/hol/kananaskis-9/kananaskis-9-logic.pdf/download
>
> Beta-conversion [BETA CONV]
> (λx. t1 )t2 = t1 [t2 /x]
> * Where t1 [t2 /x] is the result of substituting t2 for x in t1 , with
> suitable renaming of
> variables to prevent free variables in t2 becoming bound after
> substitution.
>
> Tom (and I think HOL Light) only gives the very simple beta-conversion
> inference rule
>
> (λx. a) x = a
>
> Presumably you can deduce this from the Tom's primitive inference rules,
> or maybe you need the axiom of extensionality as well. I think it's proved
> in the HOL Light sources in equal.ml:
>
> (*
> ------------------------------------------------------------------------- *)
> (* General case of beta-conversion.
> *)
> (*
> ------------------------------------------------------------------------- *)
>
> let BETA_CONV tm =
> try BETA tm with Failure _ ->
> try let f,arg = dest_comb tm in
> let v = bndvar f in
> INST [arg,v] (BETA (mk_comb(f,v)))
> with Failure _ -> failwith "BETA_CONV: Not a beta-redex";;
>
> --
> Best,
> Bill
>
>
> ------------------------------------------------------------------------------
> Learn Graph Databases - Download FREE O'Reilly Book
> "Graph Databases" is the definitive new guide to graph databases and their
> applications. Written by three acclaimed leaders in the field,
> this first edition is now available. Download your free book today!
> http://p.sf.net/sfu/13534_NeoTech
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
