Hello. This is a question concerning the formalization of “generic” structures, like a group, ring, field, topological space, vector space, and so on. That is, structures that satisfy some “axioms” and need not be unique up to isomorphism.
In the theory “ring” as found in the HOL4 library the definition of “is_ring r” requires that there is a type of elements of the ring “r”, call it “α”, and that the ring sum, product and inverse are functions “[α → ]α → α” that obey the ring axioms. It appears that if one wants to use this theory, one must have such a type “α”. Consider the case that I do not have such a type a-priory. Instead I have a larger type “β” where the elements that satisfy the predicate “P:β → bool” form a ring. Is there any way to apply the ring theory from the HOL4 library to this “subset” of β? If ringTheory used a predicate to represent ring elements “P:γ→bool” instead of a type, then there would be no such problem. Obviously this would require that the theorems of ring use the restricted quantifiers (“∀::P…”, “∃::P…”, et cetera). What is the reason that several theories in the HOL library use the approach of “type as the elements of the ring/topology/etc.” instead of “predicate as the sets of elements of the ring/topology/etc.”? Additionally, when one has a predicate and functions defined over the same type (as in my ring example above) that meet some algebraic axioms, is it always possible (in HOL4) to define a *type*, for which *all* elements meet the same algebraic axioms? 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
