Re: Ghilbert stuff

[Adam Bliss]

(+cc the group so folks know things are going on)

On Sep 4, 2012 10:22 AM, "Raph Levien" <raph....@gmail.com> wrote:

> (1) Most of these new theorems are named exactly the same as their inspiration in set.mm. In a couple cases, they're not identical (sbceq12 for example) because I don't have a separate concept for "sb" and "sbc" like Norm does.

Yeah, I never understood Norm's naming either :/  ... though perhaps nobody ever understands anyone else's names when they're so short.

> (2) Substitution is a powerful tool but tricky to work with. At this layer, as I'm sure you've found, it's easier to work with terms of the form x = A -> (ph <-> ps). But I think a little more automation might tip the scales, as simplifying [A/x](...) is something that can be done mechanically and has a simple UI. But for that to be pleasant, I think the automation needs to hide the rwff steps completely - one advantage to the former form is that you can infer rwff from it when necessary.

Yes, I agree completeley.

> Other news, and musings:
>
> I've pushed a pile of changes to theorem display and listing. It's still pretty bare, but at least it's clean now. http://ghilbert-test.appspot.com/listthms is your test url (although I expect the paths to change, because I want to explicitly name the module).

> Note how bare the description list is :) Adding a one-line description to each thm will help a lot, I think.
>

Cool, I'll take care to add more descriptions.

> Obviously one of the most tempting things is just go whole-hog HTML, so that (exp A B) is formatted as A^B. What's most appealing about it is of course that it's so easy - you just make sure the result is valid HTML (escaping where necessary) and toss that into an innerHTML. But there are other reasonable things that could be done.

This sounds very easy and probably Good Enough For Now.

> One other choice not to rule out would be to use mathjax. This would probably have the advantage of being a bit more interoperable with other sites that use LaTeX syntax (I'm thinking Wikipedia in particular). But I like using fine spacing to provide more visual cues for precedence and that would result in some ugly TeX. Of course, there's a lot of layout that mathjax does, like putting the bar over the square root, and of course matrix-like layouts, but I'm thinking it's easy to live without that for now.

Sounds intriguing but I don't know enough about mathjax to weigh in.

> And I think we can rule out MathML. Bleah.

Agreed.

> A few more random questions:
>
> Any reason you do the updating of the proof stack on keyup rather than keydown? I'm wondering if you're confused a little with button behavior on mouse clicks, where the action is on down. For key events, keyup is usually a no-op. If you're worried about lag in textarea responsiveness, I'm pretty sure a better way to do it would be settimeout with a near-zero delay.

I don't remember my original reason; confusion is a likely explanation.  But when I tried to change it recently, I ran into problems with the way electric parens handle their excursion.  If it's chafing you I can dig deeper and fix it all up.  While I'm at it I'd like to add some more fanciness such as autoindent, and maybe autocomplete.

> Any particular reason you didn't define (recurse S A B) as (iota {x | (recursep S A B x)})? It seems to me it might reduce the amount of quantifier slinging and dealing explicitly with iota. But maybe not, just curious.

I was just too focused on getting to exp to think about all the other uses for recursep. :)

But yes, it should be your way: the meat of proofs of exp0 and expsuc should be generic proofs about recurse.  Feel free to fix it up if you like.  Though one problem with using git as the authoritative theorem store is that it's harder to go "back in time" like this.

--Adam

[Adam Bliss]

Hi Raph! I have some questions about this old thread:

On Sat, Sep 1, 2012, 02:26 Raph Levien <raph....@gmail.com> wrote:

Keep in mind rwff was an experiment, to see if ax-11 was truly essential. One way to automate it away would be to include ax-11 in the axiomatization of predicate calculus. This would make it so that the axioms can no longer check unmodified in the set.mm universe, as you'd need some kind of automation to fit it. This automation could be automatically adding rwff hyps to thms that need it, or, in a totally different direction, adding x e. NN -> assumptions to every single term in the system. I can say from personal experience that having to do that manually is a real pain, and that rwff is a lot easier. But maybe the interesting observation here is that with the proper automation it wouldn't make much difference either way, and this fact is a good argument for having automation rather than working at the bare Ghilbert level.

I assume you're referring to this ancient artifact which has been in peano_min.ghi since I first saw the file:

#stmt (ax-11 () () (-> (= x y) (-> (A. y ph) (A. x (-> (= x y) ph)))))

This seems like a direct quote of http://us.metamath.org/mpeuni/ax-12.html , which brings me to my first question: why is it called ax-11 instead of ax-12?

I'm experimenting with adding this into peano_min.ghi and trying to prove substitution metatheorems like e.g. http://us.metamath.org/mpeuni/sbn.html . (One reason I'm trying this is that I already have an automation system for applying metatheorems to move around in a sexp tree, and I want to see if I can re-use it rather than maintain a second automation which mechanically applies substitution rules the way you described (which is also, I think, the way Paul's js works). For this, I want sbn and its ilk to be actual metatheorems.).

So far, I've been unable to do it. One reason that seems to be blocking me is that both x and y are binding variables in this axiom. The form of the axiom I really seem to want (and the form that undergirds the proof of sbn in set.mm) is the analogue of to http://us.metamath.org/mpeuni/equs5.html , where y can be a term variable. 

Additionally, as far as I can tell, ax-12 in set.mm doesn't seem to be used for much *besides* proving equs5. So now I'm wondering, would something like this be a more appropriate addition to peano_thms.ghi?

 

stmt (ax-12a () ((A x)) (-> (= x A) (-> ph (A. x (-> (= x A) ph)))))

or, even more directly what I want (though provable, I think, from ax-12a and ax-tyex):

stmt (ax-12b () ((A x)) (-> (-. (A. x (-> (= x A) (-. ph)))) (A. x (-> (= x A) ph)))

What do you think?

[Norman Megill]

On Sunday, March 31, 2019 at 12:49:40 AM UTC-4, Adam Bliss wrote:

Hi Raph! I have some questions about this old thread:

On Sat, Sep 1, 2012, 02:26 Raph Levien <raph....@gmail.com> wrote:

Keep in mind rwff was an experiment, to see if ax-11 was truly essential. One way to automate it away would be to include ax-11 in the axiomatization of predicate calculus. This would make it so that the axioms can no longer check unmodified in the set.mm universe, as you'd need some kind of automation to fit it. This automation could be automatically adding rwff hyps to thms that need it, or, in a totally different direction, adding x e. NN -> assumptions to every single term in the system. I can say from personal experience that having to do that manually is a real pain, and that rwff is a lot easier. But maybe the interesting observation here is that with the proper automation it wouldn't make much difference either way, and this fact is a good argument for having automation rather than working at the bare Ghilbert level.

I assume you're referring to this ancient artifact which has been in peano_min.ghi since I first saw the file:

#stmt (ax-11 () () (-> (= x y) (-> (A. y ph) (A. x (-> (= x y) ph)))))

This seems like a direct quote of http://us.metamath.org/mpeuni/ax-12.html , which brings me to my first question: why is it called ax-11 instead of ax-12?

What used to be called ax-11 is now called ax-12.  In Dec. 2018, there was a "great renaming" of the axioms because the old numbering had gaps caused by some axioms that were found to be redundant over the years, and also I wanted a clean separation between Tarski's original axiom schemes and the additional but logically redundant axiom schemes added to set.mm in order to be able to prove more general schemes ("metalogical completeness").

The correspondence between the old and new axiom numbering is here:
http://us.metamath.org/mpeuni/mmset.html#oldaxioms

This renumbering was the result of a year-long discussion and wasn't done lightly.  In particular, it affects some papers and other write-ups that reference the old numbering.  The original axiom numbering was in place for 25 years but was beginning to show its age for the reasons above.  So I hope the "great renaming" is a once in a lifetime event that will survive indefinitely.

BTW the separation between Tarski's and our additional axiom schemes is given here:
http://us.metamath.org/mpeuni/mmset.html#pcaxioms
 

I'm experimenting with adding this into peano_min.ghi and trying to prove substitution metatheorems like e.g. http://us.metamath.org/mpeuni/sbn.html . (One reason I'm trying this is that I already have an automation system for applying metatheorems to move around in a sexp tree, and I want to see if I can re-use it rather than maintain a second automation which mechanically applies substitution rules the way you described (which is also, I think, the way Paul's js works). For this, I want sbn and its ilk to be actual metatheorems.).

So far, I've been unable to do it. One reason that seems to be blocking me is that both x and y are binding variables in this axiom. The form of the axiom I really seem to want (and the form that undergirds the proof of sbn in set.mm) is the analogue of to http://us.metamath.org/mpeuni/equs5.html , where y can be a term variable. 

Additionally, as far as I can tell, ax-12 in set.mm doesn't seem to be used for much *besides* proving equs5.

This used to be the case, but it now serves also serves to prove what used to be called ax-10, now theorem http://us.metamath.org/mpeuni/axc11.html , that seems to be needed for "metalogical completeness" (in particular the ability to bundle variables).

While I'm not sure if your proposals are weaker or equivalent, whether a weaker variant of ax-12 will do for your purposes depends partly on whether you consider the ability to bundle variables important for your system.  In addition, because it is logically redundant, ax-12 can be dispensed entirely in principle.  The closest you can get to ax-12 from Tarski's system seems to be http://us.metamath.org/mpeuni/ax12w.html, which allows you to derive any substitution instance of ax-12 in which there are no wff metavariables and all individual variables are mutually distinct.  An example of how to do this is provided by http://us.metamath.org/mpeuni/ax12wdemo.html.
 

[Raph Levien]

What Norm said. In my later Ghilbert explorations (which, sadly, have not gotten to the point of a usable system), I'm moving very much away from Tarski-style distinct variables and towards variable binding that works basically the same as lambda calculus (perhaps with even alpha conversion built in).

I can't figure out just from looking whether your alternate axioms would work for your needs. They're almost certainly valid, but it depends on exactly what you want in the logic and what in the metalogic, and whether you plan to translate into or out of other logical systems (this is why I'm moving more in a lambda direction).

Best of luck, I'm interested to see what you come up with.

R

--
You received this message because you are subscribed to the Google Groups "Ghilbert" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ghilbert+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Adam Bliss]

Norm, Raph, thanks for the replies. One of the main things I'm still confused about is whether my proposed modifications are in fact conservative. In set.mm, it certainly seems like they would be. But in Ghilbert, you can take a metatheorem expressed with a binding var (which does not happen to be quantified), and replace the binding var with a term var of the same kind, while keeping the exact same proof, and actually strengthen the metatheorem. (I think this doesn't happen in set.mm because all setvars are quantifiable and all wffs are expandable, and never vice versa?)

If we had an operative isomorphism between Ghilbert and Metamath, I would try to translate the proof of equs5 from ax-12. But the theoretical isomorphism has always been especially hazy to me around the topic of Term Vars.  

(I've also been thinking a lot about switching to a lambda-based variable binding scheme. Trying to do proper substitution in my Tacro engine has exposed several bugs in the way I was handling FreeMaps.)

Anyway, thanks again; I'll keep you posted if/when I figure something useful out.

--Adam