On Thu, Sep 26, 2019 at 6:01 PM David A. Wheeler <[email protected]> wrote:
> On Thu, 26 Sep 2019 16:56:26 -0400, Mario Carneiro <[email protected]> > wrote: > > The main worry I have about a pure reimplementation is the > > automated theorem prover part. > > I added a hypertext link from the conventions text to the JavaScript code. > That way, someone who wants to know more will be able to quickly > see more information. That's not the best way to define things, > but I think the current problem is that it's not obvious that this > situation > even exists or how to get *any* information about it. > The definition of correctness here is not hard: you just assert that a particular theorem is true, or provable. The hard part is having an algorithm that is sufficiently good to actually be able to find such proofs sufficiently often that it isn't spuriously rejecting definitions all the time. > > If you aren't worried about dependence on set.mm metatheory, or on > actually > > producing proofs, the easiest algorithm to implement is to keep track of > > all binding operators, and ensure that all dummies are not free in the > true > > sense (while also calculating the binding structure of the new > definition). > > Is that algorithm adequate? > It is, and it's less flaky than one that is dependent on there being enough theorems in the database to be able to prove the relevant F/ theorems. There is a metatheorem that asserts that whenever a variable is properly not free in a term then the appropriate F/ theorem is provable, and from there you can prove that P(x) <-> P(y) holds where x is the variable that is not free in P. The metatheorem corresponds to a particular proof, that can be constructed by recursion on the term P, but we aren't putting that proof anywhere right now and for conservativity it only matters that such a proof exists, so we may as well be satisfied with the metatheorem and not generate the proof at all. The code seems to all depend on proveBoundVar (copied below), but > I've never written an mmj2 JavaScript plugin so I wasn't sure how > to interpret that code (and it'd take me some time to drill in). > Oh, I guess I forgot; boundVars in that algorithm is actually the information about whether each set variable is bound in a syntax constructor. So actually mmj2 isn't proving F/ theorems all the time; it only does so when it can't derive the bound variable status of a definition, usually because it's an axiomatic term like "A. x ph". In these cases it falls back on the "fast = false" case where it actually attempts to search the database for a proof of "A. x ph -> A. x A. x ph", and if it finds a proof then it marks x as not free in ph. If it was not able to find a proof then it says that x is (potentially) free in ph in "A. x ph", which would then cause later definitions using a dummy under a forall binder to fail. The "theorem proving" in this case is actually trivial; it's looking for an exact match with a given theorem statement. There is no index saying "here is the proof of |- ( E. x ph -> A. x E. x ph )" so I'm using the mmj2 one-step theorem prover to do the matching, but this is the sort of thing where a well positioned $j annotation can just say "you want the F/ theorem for df-ex? Try nfex" and skip the library-wide search. Mario -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsvcAmz4xrwS2Y0%3DB1uzKe71Su7-X-0LKbEPbZvMZb-VA%40mail.gmail.com.
