On 22/01/18 18:35, Cris Perdue wrote: > Are any of you readers of this list aware of investigations or > implementations of logics that, like the HOL family of provers, are based > on the simple theory of types, but which support introduction of new types > through new predicates rather than new type constants? Presumably numbers > then could be individuals, like other individuals, with some being > integers, some real, and so on.
Hello. I really do not understand what you are looking form. If you want something like “subtypes”, you can use restricted quantification (theory "res_quan"). E.g. You can define a term “ODD:(num -> bool)” and then quantify as in “∀x::ODD. P x”. However, many tactics in HOL4 are blind to restricted quantification. Fixing this it is just a matter of making a change in the source code or writing a wrapper. In my repository of HOL4 developments <https://puszcza.gnu.org.ua/projects/hol-proofs> have a wrapper for “MESON_TAC” and a tactic that is like “MATCH_MP_TAC” but extended in that it adds support for restricted quantification and other things. Alternatively, you can embed a type system with coercing/casting functions. E.g. You have a function “COERCE_ODD (:num -> :num)” which returns the same number of it is odd, and an arbitrary odd number otherwise. Then to quantify over odd numbers, you write “∀x. P (COERCE_ODD x)” instead of (with the above approach) “∀x::ODD x”. As far as I know: Simple type theory has no means to introduce new types; that is a conservative extension found in some proof assistants like HOL4. The types in Church's formulation [1] are the individuals (type “ind” in HOL4), propositions (roughly type “bool” in HOL4; but Church allows the possibility of intensional propositional functions), and the scheme: if “'a” and “'b” are types, then “'a -> 'b” is a type. I would like to share some of my observations regarding type theories compared to set theories: If you want, roughly speaking, that all objects are treated the same (as “individuals”), set theory already does that. I am aware that a common complain against set theory is the existence of “junk theorems” like “0 ∈ 1” (E.g.: this holds if 0 and 1 are ordinals with the usual Mirimanov-von Neumann construction, or reals with the Dedekind construction). But this is unfounded. In a proof assistant based on set theory with atoms (a.k.a. “urelements”) one could in principle add (akin to type definitions in HOL4) new sets of atoms disjoint from the set of all previously-defined atoms; then objects that are conceptually not sets (numbers, etc.) could be introduced as atoms and there would not be “junk theorems”; this is like a typical type theory, but instead of having bad-typed formulas, you would have theorems of non-elementhood like “∀S. 1 ∉ S”. Another complaint against well-founded (Zermelo-style) set theories is that in general, the set of all {groups, topological spaces, categories, etc} is not itself a set. The set theory New Foundations, which is not well-founded, has a set of all sets, but the price it pays is that in general separation does not hold (i.e.: There exists a set S and formula P in which x is free, for which {x | x ∈ S ∧ P} is _not_ a set). I hear that it has problems with constructions like “the set of all categories” but I have not investigated into that. By contrast, I am not aware of any type theory which has a equivalent of an universal set. Usually either there are terms without a type, or “kinds” that are not types, which is the antithesis of an universal set/type. Polymorphism gives _the illusion_ that one has the set of all sets _and_ at the same time the separation axiom; but it is just an illusion, for if that was really the case the system would contain a contradiction (i.e.: Russell paradox). For example, in HOL4 you have the seemingly universal type {x | T}; and for any P, if “{x | P x}” is well-typed then it is a “set”). “UNIV ∈ UNIV” is provable; yet the occurrences of “UNIV” have different types; trying to derive “∃S. S ∈ S” fails because it is not even a WFF. Polymorphism is usually found in type theories, and it is usually hidden by the printer so it is not very conspicuous, thus enhancing the illusion of a very expressive theory. But this is just the current trend. One can polymorphism in set theory too. In a vague sense, New Foundations can be seen as having polymorphism “built-in”. It can be added to ZFC if one restricts the scope of quantifiers to sets. If you add classes (as in NBG) and pretty-printing on top, it can too give the illusion of having universal comprehension. Now, I _imagine_ that by a suitable limitation of quantification one could have a set of atoms “True” and “False” in a ZFC+atoms and then have propositions as ordinary functions. However I have not explored this possibility. In my opinion, sophisticated type theories (specifically, those with types that can depend on terms, like the Calculus of Constructs) merely make more complex what can be already expressed in set theory (incl. set-based model theory) but making it seem as it was something “deep” with syntax tricks (e.g.: intentional conflation of terms and proofs). We can already see this phenomenon (a theory that seems better; yet is not on careful examination) with classical second-order logic: It seems more “expressive” than first-order logic until you realize that all computable formulations of second-order logic have the same shortcomings as first-order logic (E.g.: A computable second-order logic can be complete w.r.t. frugal models, never w.r.t standard models; and with frugal models you again have Skolem paradox and non-standard models for second order PA). Set theory has given us deep theorems with relevance outside itself, like the independence of the choice axiom, and relative consistency proofs for weaker systems like PA. I am not aware of any result like that coming from type theory. [1]: “A Formulation of the Simple Theory of Types”. Alonzo Church; 1940. > Any references to results of existing efforts to explore the potential > and/or issues raised by such arrangements would be much appreciated. > > A significant part of my own interest in this approach is related to > usability by non-specialists, and in that sense style might be more an > issue than ultimate expressive power. Ideally such a system would also > support a relatively flexible and rich system of "types", without the need > to bring in the conceptual complexity of dependent types, and their > accompanying notations. > > Best regards and thanks in advance, > Cris
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
