Dear Rob,
Thank you for supporting my position here ("However, I agree that there are
many useful properties that are best specified using more general
quantification over types.").
Let me remind you that you pointed out some time ago the fact that the implicit
universal quantification over the free type variables in HOL make certain
expressions unworkable, namely that the appeal to the axiom of choice can't be
made explicit in the form AC => THM because of the free type variable in the
hypothesis:
https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2018-03/msg00043.html
With quantification over types this is possible (since the type variable isn't
free anymore):
https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2018-03/msg00051.html
The proof is still available online:
https://www.kenkubota.de/files/ac_instantiation.r0.out.pdf
Note that the Quantified Axiom of Choice (without a free type variable)
∀τ[λt.AC]o
(wff 1388 = QAC)
is to be read as
∀ t . AC
where "t" is the type variable in question here.
Regards,
Ken
____________________________________________________
Ken Kubota
https://doi.org/10.4444/100
> Am 16.01.2023 um 21:08 schrieb Rob Arthan <r...@lemma-one.com>:
>
> Dear All,
>
> A couple of points in this connection:
>
> 1) Maybe it has already been mentioned in this thread, but if not, people
> should be aware of Peter Homeier’s HOL Omega, which attempts to address the
> issue under debate (and I think was in part inspired by Mike Gordon’s
> observations about lambda-abstraction over types).
>
> 2) With the existing polymorphism, you can define classes of structures such
> as “all groups”, because that doesn’t require anything more than an outermost
> universal quantifier over type variables, which is what HOL as is gives you.
> (E.g., see my paper on group theory in ProofPower-HOL:
> http://www.lemma-one.com/ProofPower/examples/wrk068.pdf.) However, I agree
> that there are many useful properties that are best specified using more
> general quantification over types.
>
> Regards,
>
> Rob.
>
>> On 16 Jan 2023, at 19:28, Ken Kubota <m...@kenkubota.de> wrote:
>>
>> Technically speaking, yes, but the question's implication itself is very
>> problematic.
>>
>> Why should somebody confine oneself to the obsolete and obviously
>> impoverished type system of HOL (Church's logic, slightly modified)?
>> Why should the scientific community blatantly ignore the obviously correct
>> hints from Mike Gordon, the founder of HOL, on future developments?
>>
>> The limitations of HOL are well known, criticized by many people (Freek
>> Wiedijk: "The HOL type system is too poor. As we already argued in the
>> previous section, it is too weak to properly do abstract algebra." / John
>> Harrison et al.: "Another limitation of the simple HOL type system is that
>> there is no explicit quantifier over polymorphic type variables, which can
>> make many standard results like completeness theorems and universal
>> properties awkward to express").
>>
>> For example, with lambda abstraction over types the fact that (Z, +) is a
>> group can be expressed naturally as
>> Grp Z +
>> which is what a mathematician wants. But this is not possible in HOL.
>>
>> My example was formally proving the theorem
>> Grp o XOR
>> expressing the fact that (o, XOR) is a group:
>> https://www.owlofminerva.net/files/formulae.pdf#page=420 (wff 6955 =
>> XorGroup)
>>
>> For the group definition see
>> https://www.owlofminerva.net/files/formulae.pdf#page=362 (wff 266 = Grp)
>> and for some explanation
>> https://sympa.inria.fr/sympa/arc/coq-club/2022-06/msg00025.html
>>
>>
>> Of course, from an engineering perspective (for practical purposes like
>> smart card applications), formalizing/automating HOL theorems or theorems of
>> first-order logic still has its legitimacy.
>>
>>
>> But from a scientific perspective, formalizing/automating 1940 type theory
>> has its limits.
>>
>>
>> ____________________________________________________
>>
>> Ken Kubota
>> https://doi.org/10.4444/100
Full thread:
https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2023-01/msg00039.html
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
