On 24/01/18 14:47, Cris Perdue wrote: > As it turns out, I am not using HOL4 at all, but a system I have been > writing bit by bit for some time, in JavaScript running in modern web > browsers, [...]
> Aside from implementing basics of pure logic, the real numbers have been > its focus so far, though I have been stubborn enough not to limit the > design to just working with a single theory such as numbers. From near the > beginning it has used a predicate "R" for real numbers. Its rewriting rules > work with conditional equations, e.g. R x & R y => x + y = y + x, and it > automatically reduces assumptions such as R (x * y) to R x & R y as they > occur. From what you described here, it seems that the system you describe is noticeably similar to HOL4 (and probably HOL Light too but I have not used the later); If I recall correctly, HOL4 logic and Q0 (with extensionality) effectively differ only in that Q0 has no mechanism to introduce user definitions and does not have Hilbert ε. I do not recall if Q0 has type polymorphism, like HOL4. Like your system, HOL4 has term rewriting, and it uses a sequent calculus (i.e. handles assumptions at the level of the logic). You may find it useful to take a look into HOL4 or HOL Light and then copy (probably that would be re-implementing them in JS) the features you find useful instead of developing them from scratch. Do you want to have a _single type_ for all atoms (the “type of atoms”)? If so, then I imagine you can introduce a mechanism of definition for new sets of atoms, like type definition in HOL4, but that instead of introducing a new type, it introduces an axiom asserting the existence of a set of atoms disjoint from all previously introduced sets of atoms and in bijection with the user-provided representation (like “new_type_definition” followed by “define_new_type_bijections” in HOL4). Although this appears to be straightforward, I can not assure you it is, and I do not know the details of this approach. > It is not intended as an aid for sophisticates such as typical members of > this list, but for people inexperienced with interactive theorem proving, > whose exposure to mathematical notation and mathematical reasoning may be > limited to ordinary high school math education and ordinary (let's say > American) math textbooks. If I understand you correctly, your target audience is people without special preparation nor interest with mathematics. This means that they do not even know what a formal system is, and thus they either have no idea of what a proof is, or an erroneous one. I doubt that this people is interested in proof assistants. Do you know Metamath <http://us.metamath.org/mpeuni/mmset.html>? If not, maybe you want to take a look since it is supposed to be understandable with minimal prerequisites. A common mention in the numerous prefaces of mathematical books (e.g.: the book of Mendelson that I referenced) is that there are no strict prerequisites but knowing X or Y is suggested to “understand” it or have a motivation for definitions and theorems that would otherwise look disconnected from anything else. The same comment applies to any proof assistant with no strict prerequisites. > A little passage from a well-known old paper by Dana Scott gives me some > encouragement as well. In "A type-theoretical alternative to ISWIM, CUCH, > OWHY", written in 1969 but only published in 1993, he comments: [...] I can not comment on this because I am not familiar with that paper. > Just a couple of short comments on the attractions of type theory. For me, > the axioms of Q0 in particular are models of what axioms ought to be. In > type theory, functions and predicates are fundamental, so except perhaps > for Currying, the road is immediately open to working with traditional > statements about numbers and other concepts as well. And of course > Russell's Paradox is not an issue, as you point out. I think derivatives of lambda calculus like Q0 and HOL4 can easily give a misleading impression by treating functions as fundamental concepts (Note that propositions are just functions with range “bool” in Q0 and HOL4). The presentation of axioms make it seem as if they captured the properties of all functions (incl. propositions) with a simple set of a axioms, yet this is provably impossible. See §6 of <http://imps.mcmaster.ca/doc/seven-virtues.pdf> and Appendix A of “Introduction to Mathematical Logic, ed. 6”, Elliot Mendelson 2015[1]. By contrast, first order logic is “complete” in the sense that a proposition is provable iff it holds for all models. There exists a formulation of semantics for which higher order logic is complete too, which does not interpret quantification of functions as real quantification (called Henkin semantics; this is usually treated in the context of second-order logic; the reasoning for higher order logic is similar). Also, note that usually one works in a theory that has uncountably many functions, yet only countably many functions can be described by syntax (any logic with a countable set of WFFs is the same in this regard). For example, the set/proposition/type, of propositions over the natural numbers (i.e.: functions from N to bool) is easily shown to be uncountable by Cantor diagonal argument. Thus, if the universe includes uncountably many functions then lambda terms (or any other notation with a finite alphabet and finite strings) are unable to describe the vast majority of functions (uncountably many!). The same applies to real numbers since they are uncountable too. > I do appreciate the important contributions set theory has made to > mathematics. Beyond that, foundational issues such as fitting category > theory into mathematical foundations are immensely intriguing, but I think > it unlikely that I myself will have the opportunity to properly grasp the > issues, at least not in this lifetime. I am not knowledgeable in that, yet I doubt that the issue is very complex; Concepts like “the set of all groups/categories/etc.” are usually (or always?) not sets in ZFC (but they are proper classes in NBG, which is a conservative extension of ZFC) because of cardinality. Say you want “the set of all groups”. NBG and ZFC have separation (for any set A and a predicate P, {x | x ∈ A ∧ P x} is a set) and foundation. Together these give us an useful heuristic to reason about them (search “cumulative hierarchy” if you are interested), but it means that self-referential concepts typically can not be embodied. The simplest one is maybe the Burali-Forti’s paradox. A very very rough explanation is as follows: suppose you represent whole equivalence classes of well-ordered sets by a single set. then suppose there was “a set of all well-ordered sets” (it is not a set in ZFC but it is a proper class in NBG). This is itself a well-ordered set when the order is defined by one element of _this_ set being an initial segment of another. By construction, this set includes any other subset as a proper initial segment, including itself; thus we have proven by contradiction that aforementioned construction does not exist. Regards. [1] Library Genesis <http://gen.lib.rus.ec/> has this book.
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
