Hello Mario,
Thanks for your various comments, suggestions, and thoughts. Where I have a
response, they are below, inline.
On Fri, Jan 26, 2018 at 7:45 PM, Mario Xerxes Castelán Castro <
marioxcc...@yandex.com> wrote:
> 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.
>
Good advice I'm sure, at least on general principles. I tried to study HOL
Light maybe four years ago with something like this in mind, but the effort
was not a success, though it left me with considerable respect for the work
that went into HOL Light. Such an effort might succeed better for me with
HOL4, but I have not attempted it.
>
> 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.
>
Yes, that is what I am seeking.
>
> > 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.
>
Well no. If a person has neither special preparation nor interest, I would
not wish to bother them.
On the other hand, I do believe that it is possible for a sufficiently
well-engineered proof assistant to become useful to students with much less
special preparation than is required today, but the possibilities and
tradeoffs would be a complex discussion.
>
> 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.
>
Yes, I am fairly familiar with Metamath. Its mechanisms are simple and its
community has achieved some impressive things. I don't consider it a
suitable vehicle for my needs, but once one learns to interpret its
language and follow its proof steps, the proofs can be pretty readable.
Best regards,
Cris
------------------------------------------------------------------------------
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
