Email Gateway (Aug 23 2022 at 09:24): Email Gateway (Aug 23 2022 at 09:24):From: Ken Kubota <mail@kenkubota.de>
As I do not expect any substantial new argument, let me shortly summarize my account on representing type dependencies in Isabelle/HOL and in dependent type theory.
While I have always emphasized that the logical foundation should be a further development of Q0, with expressiveness as the main criterion for the design (hence, Hilbert-style, use of the description operator, no implicit use of the Axiom of Choice),
(Peter B. Andrews: A Formulation Based on Equality – https://owlofminerva.net/sep-q0 <https://owlofminerva.net/sep-q0>)
(Andrew M. Pitts on HOL vs. Q0: “From a logical point of view, it would be better to have a simpler substitution primitive, such as ‘Rule R’ of Andrews’ logic Q0, and then to derive more complex rules from it.” – https://owlofminerva.net/files/fom_2018.pdf#page=6 <https://owlofminerva.net/files/fom_2018.pdf#page=6>)
(Mike Gordon on the use of the epsilon operator in HOL: “It must be admitted that the ε-operator looks rather suspicious.” “The inclusion of ε-terms into HOL ‘builds in’ the Axiom of Choice [...].” – https://owlofminerva.net/files/fom_2018.pdf#page=9 <https://owlofminerva.net/files/fom_2018.pdf#page=9>)
it is also clear that for interactive theorem proving or automation, a natural deduction variant is required, and a meta-logic is desirable in order to symbolically represent metatheorems employing a symbol for derivability/provability.
(Lawrence C. Paulson introducing ‘meta-implication’ – https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf#page=5 <https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf#page=5>)
The task of the meta-logic is exploring the properties of a given (object) logic, i.e., expressing metatheorems which are inexpressible within the object logic, and also the theorems of the logic themselves, which can be expressed in the form of a metatheorem.
However, concerning the use of the meta-logic in HOL-Algebra (group theory: abstract algebra), the case is entirely different.
Emulating type restrictions and type dependencies as set-theoretic conditionals in Isabelle's meta-logic is an attempt to enhance the given object logic, and clearly contrary to the approach of type theory, where such conditions are syntactically represented.
One may accept this as a preliminary workaround, but in general, representing these type restrictions and type dependencies is a matter of the underlying object logic (in this case type theory).
I have positively shown that group theory can be naturally expressed in type theory (using type abstraction) – https://www.owlofminerva.net/files/formulae.pdf#page=362 <https://www.owlofminerva.net/files/formulae.pdf#page=362>.
So as long as the object logic is insufficient, one may accept the auxiliary approach of using set-theoretic conditionals in the meta-logic as a workaround, which is obviously opposed to the very idea of type theory, in which these restrictions (e.g., the closure of the operation and of the unit in groups) are expressed syntactically as types within the object logic (and not as meta-logical implications in the meta-logic).
But one should be aware of the fact that this emulation is only a preliminary workaround, not a satisfying solution.
The deficits of the (current) HOL family are well known.
(Freek Wiedijk on the (current) HOL family: “The HOL type system is too poor. As we already argued in the previous section, it is too weak to properly do abstract algebra.” – https://owlofminerva.net/files/fom_2018.pdf#page=10 <https://owlofminerva.net/files/fom_2018.pdf#page=10>)
(John Harrison, Josef Urban, and Freek Wiedijk on the (current) HOL family: “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 [...] awkward to express [...]. [...] For example, in one of the most impressive formalization efforts to date [Gonthier et al., 2013] the entire group theory framework is developed in terms of subsets of a single universe group, apparently to avoid the complications from groups with general and possibly heterogeneous types.” – https://owlofminerva.net/files/fom_2018.pdf#page=10 <https://owlofminerva.net/files/fom_2018.pdf#page=10>)
Using the enhanced expressive power gained from the meta-logic of a logical framework such as Isabelle for compensating the deficits of the object logic (with a deprecated type system) and, after that, defending the obviously impoverished type system, is unacceptable.
Ken Kubota
https://doi.org/10.4444/100
Last updated: Nov 21 2024 at 12:39 UTC