Progress: HTML theorem display with interactivity

[Raph Levien]

I've made a fair amount of progress towards my goal of nicer HTML display of theorems. It's still rough and there's more I want to do, but I figured now is as good a checkpoint as any.

It's relatively easy to build from source, but I've also put files up on static serving:

http://ghilbert.org/gen/bitri.html

Hovering over a proof step highlights the "arguments" of the step. Clicking on it brings up an info card. There's lots more that I want to put on the card (the statement of the theorem, the explicit substitution of the variables), but the fact that it displays the result line is a start.

Also note that the translation from Metamath is cruder than I'd like - it puts a label on every line whether needed or not, it makes lines for every step even if it could be inlined without parentheses.

Even though it's not quite my vision, I thought people on this list would like to see where I'm going with this.

Raph

[Cris Perdue]

Hi Raph,

Could you review for us on the list your main goals for Ghilbert these days? I've had the impression that you have an interest in making Ghilbert in some way independent of a particular logic, or supporting interchange of proofs done in different logics?

By the way, I have admired your analysis of "bundling" of theorems in Metamath. If it is feasible to do, I would love to see a display of the multiple conventional theorems bundled into a Metamath theorem where this is the case.

Cheers,

Cris

--
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+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Raph Levien]

Hi Cris,

I've written a draft of the goals here, but I'm not very satisfied with the document: http://ghilbert.org/why.html . But it should be something of a start. Comments and discussion are welcome (I've already gotten some good feedback which I haven't integrated yet).

Yes, I want to support different logics, and in interchange. Lately I'm interested in supporting intuitionistic logic, so that proofs can be exported to Idris and Lean (the latter does support classical logic, but not by default).

I haven't gotten to the bundling just yet; I'm pushing on the fragment without bound variables for now. When I do, I'll try to have a reasonable presentation. Incidentally, one of the things that's missing from the current prototype is proper links back to the Metamath pages; not intentional, just something I haven't gotten around to doing yet.

Take care,

Raph

[Jim Kingdon]

With respect to intuitionistic logic, I trust people have seen http://wikiproofs.org/w/index.php?title=Interface:Intuitionistic_propositional_logic ? It is a development very much analogous to the propositional logic in metamath's set.mm. Even adds in the law of the excluded middle and proves the "missing" theorems (in a straightforward way, rather than by going back to classical propositional logic axioms or the like) - http://wikiproofs.org/w/index.php?title=From_intuitionistic_to_classical_propositional_logic

It is done in JHilbert (which is based on a rather old version of ghilbert), but that's not the interesting part. The interesting part (at least for me) was seeing how much of set.mm's propositional calculus carries over to intuitionistic logic, and how some of your classical habits can be replaced by ones which work intuitionistically.