[opentheory-users] axioms or proofs?

[Ramana Kumar]

I suspect ETA_AX cannot be derived in HOL Light (i.e. the formulation
with only equality as primitive), but maybe can in other formulations.
Or were you thinking of IMP_ANTISYM_AX, Konrad?

On 3 June 2015 at 21:42, Joe Leslie-Hurd <joe at gilith.com> wrote:
> 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
>>>
>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list