[opentheory-users] axioms or proofs?

[Joe Leslie-Hurd]

For some reason ETA_AX is still an axiom in HOL Light, together with
SELECT_AX and INFINITY_AX.

All this proof snippet does is write the axiom in terms of the
primitive symbols (the only primitive constant is =) and then derive
the usual presentation of the axiom from the primitive one. This trick
is used to ensure that the primitive axioms of OpenTheory do not
depend on the definition of any symbol.

Cheers,

Joe

On Wed, Jun 3, 2015 at 9:49 AM, Konrad Slind <konrad.slind at gmail.com> wrote:
> ETA_AX used to be a primitive in the HOL logic, but
> someone (Bruno Barras? John Harrison?) realized that
> it could be proved from the other axioms. Since
> removing unnecessary axioms is thought to be
> a good thing, it was made into a proved theorem.
>
> Konrad.
>
>
> On Wed, Jun 3, 2015 at 11:00 AM, Robert White
> <ai.robert.wangshuai at gmail.com> wrote:
>>
>> Dear Joe,
>>
>> Is there any reason why you want to change some axioms in the files as
>> "proofs"?
>> For example:
>>
>> let ETA_AX =
>>   let axiom =
>>       let ty0 = mk_vartype "A" in
>>       let ty1 = mk_vartype "B" in
>>       let ty2 = mk_fun_ty ty0 ty1 in
>>       let ty3 = mk_type ("bool",[]) in
>>       let ty4 = mk_fun_ty ty2 ty3 in
>>       let tm0 = mk_var ("a",ty4) in
>>       let tm1 = mk_var ("b",ty2) in
>>       let tm2 = mk_var ("c",ty3) in
>>       let tm3 = mk_abs (tm2,tm2) in
>>       let tm4 = mk_eq (tm3,tm3) in
>>       let tm5 = mk_abs (tm1,tm4) in
>>       let tm6 = mk_eq (tm0,tm5) in
>>       let tm7 = mk_abs (tm0,tm6) in
>>       let tm8 = mk_var ("d",ty2) in
>>       let tm9 = mk_var ("e",ty0) in
>>       let tm10 = mk_comb (tm8,tm9) in
>>       let tm11 = mk_abs (tm9,tm10) in
>>       let tm12 = mk_eq (tm11,tm8) in
>>       let tm13 = mk_abs (tm8,tm12) in
>>       let tm14 = mk_comb (tm7,tm13) in
>>       new_axiom tm14
>>   in
>>   prove
>>     (`!(t:A->B). (\x. t x) = t`,
>>      PURE_REWRITE_TAC [FORALL_DEF; T_DEF] THEN
>>      ACCEPT_TAC axiom);;
>>
>>
>> instead of just :
>>
>> let ETA_AX = new_axiom
>>   `!t:A->B. (\x. t x) = t`;;
>>
>> Thanks!
>>
>> --
>>
>> Regards,
>> Robert White (Shuai Wang)
>> INRIA Deducteam
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>