On 05/09/17 11:57, michael.norr...@data61.csiro.au wrote: > These are good questions. You are right that the ring and topology examples > aren’t as usable as one might like. > If you want to do real formalisations of abstract algebra, you do want to be > able to work with subsets of the whole of the type. See for example the > treatment of groups in examples/miller/groups. […] The most extensive > mechanisation of this sort of thing that I’m aware of for HOL4 is by my > student Hing-Lun Chan. You can get it from […]
Thanks for the links. These formalizations are very helpful to see how HOL4 is used in practice. Admittedly, I should have done a search with grep over the “examples” directory but I had forgot about its existence. > In principle, if you want to use a theory (rings say) that assumes the whole > type, but you want to apply it to a subset of another type, you could define > a third type that is isomorphic to your subset (this is what > new_type_definition does), and then use the results from the ring theory to > derive results about your new type. These results could in turn be translated > to the subset of the original type through the isomorphisms that the new type > principle establishes. I’m not aware of anyone trying to do this with any > seriousness. >> - The reason that the “whole type” approach is used in places is because it’s simpler to work with, and if you are not wanting to do large developments over the full theory, it can still be quite useful. > > - The restricted quantifiers could be used to write results, but the support > for these seems to get in the way more than help, so work in this area tends > to expand the restricted quantifiers with their definitions, turning ?x::P. Q > x into ?x. P x /\ Q x Understood. > - I’m not sure I understand your final question. Certainly, it is easy to > write contradictory axioms so that no type could be found to satisfy them. > On the other hand, if there is a set that satisfies the given axioms, then it > should be possible to show that a HOL type of the same cardinality does > indeed satisfy those axioms. Sorry; I should have been more clear. Consider this hypothetical situation: I have a proposition “P:σ->bool”. (P is a metavariable ranging over HOL terms with no free variables, σ is a HOL type which may contain free type variables). In addition, I have proved that the predicate-set P is non-empty (“∃ x. P x”). The question is: Under the above conditions, is it always possible to find a HOL type “τ” and a HOL term “f:σ” which is a bijection (i.e. “!y:τ. ?!x::P. f x = y” is provable) between the predicate-set P and the type τ? According to my understanding, §2.4.5 “Extension by type definition” of LOGIC describes a mechanism to introduce by definition one such type τ. My question can be informally interpreted as the question of whether such a type can always be constructed without the need for using the definition mechanism. Regards and thanks. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
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
