On 17 Mar 2014, at 00:52, Konrad Slind <konrad.sl...@gmail.com> wrote:
> 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.
Yes. I don’t know the right reference: the comment in the HOL Light
source refers to Beeson’s book. Here is the proof:
Given p:bool, you prove ?x : bool.(x = F) \/ p) and ?x:bool.(x = T) \/ p
using F and T as the witnesses and hence choice expressed in
terms of the Hilbert epsilon-operator (@) gives you:
(((@x.(x = F) \/ p) = F) \/ p) /\ (((@x.(x = T) \/ p) = T) \/ p)
That conjunction of disjunctions gives you four cases: p holds in three of the
cases,
and in the remaining case you have:
((@x.(x = F) \/ p) = F) /\ ((@x.(x = T) \/ p) = T)
In this case, if you assume p, the above simplifies to:
((@x.T) = F) /\ ((@x.T) = T)
leading to the contradiction F = T. Hence in three cases, p holds, and in the
remaining
case, p implies a contradiction, and so ~p holds. (~p is p => F, by
definition). Hence
you get !p. p \/ ~p.
Concerning beta-conversion …
> On Sun, Mar 16, 2014 at 7:25 PM, Bill Richter <rich...@math.northwestern.edu>
> wrote:
> … 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.
You don’t need anything other than Tom’s 10 rules. Note that he doesn’t give a
schematic presentation of the last two rules that let you substitute for type
and term variables, so they are easy to miss. The general beta-conversion rule
is just obtained by term substitution for x in the above special case, which is
what the code you quote below is doing (modulo an optimisation that avoids the
substitution if it is not necessary. (INST is the term substitution rule).
> 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";
Regards,
Rob.
------------------------------------------------------------------------------
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
